Conversation
Summary: Use the weak option namespace required by the pinned Lean toolchain so standalone property and audit branches can build without an unknown-configuration error. Test Plan: - lake build PiBaseLean
Summary: Introduce a generated data-only Pi-Base catalog and a persistent Lean environment registry for spaces and property certificates. Registrations are checked against elaborated declaration types with definitional equality, while the final audit reports completeness, provenance, assumptions, and transitive axioms as deterministic JSON. Test Plan: - python3 -m unittest tests/test_gen_space_audit_catalog.py - lake build PiBaseLean.Audit.Spaces.Registry - lake build PiBaseLean.Audit.Spaces.Tests.CrossModuleDuplicateSmoke Generated Files: Run meerkat after landing if repository-wide generated metadata requires refresh. Tags: stack_created_with_devmate
Summary: Keep Catalog.lean as the stable handwritten audit schema, limit catalog generation and freshness checks to GeneratedCatalog.lean, and mark generated Lean data for Linguist. Test Plan: - python3 -m unittest tests/test_gen_space_audit_catalog.py - python3 scripts/gen_space_audit_catalog.py --check - git check-attr linguist-generated -- PiBaseLean/Audit/Spaces/GeneratedCatalog.lean PiBaseLean/Spaces/S1/Generated.lean PiBaseLean/Audit/Spaces/Catalog.lean - lake env lean PiBaseLean/Audit/Spaces/Catalog.lean (pass) - lake env lean PiBaseLean/Audit/Spaces/GeneratedCatalog.lean (pass) - lake build PiBaseLean.Audit.Spaces.Tests.CrossModuleDuplicateSmoke (dependency build timed out) - lake build PiBaseLean.Audit.Spaces.Tests.RegistrySmoke (blocked by pre-existing linter option configuration before target compilation)
Summary: Exercise space and certificate registration with a synthetic discrete carrier so the registry PR validates independently of the later pilot-space implementation. Test Plan: - python3 -m unittest tests/test_gen_space_audit_catalog.py - python3 scripts/gen_space_audit_catalog.py --check - lake build PiBaseLean.Audit.Spaces.Tests.RegistrySmoke
Summary: State the synthetic certificate using its underlying topological proposition so the registry boundary compiles against the existing bundled Property API on master. Test Plan: - lake build PiBaseLean.Audit.Spaces.Tests.RegistrySmoke - lake build PiBaseLean.Audit.Spaces.Tests.CrossModuleDuplicateSmoke
Deicyde
force-pushed
the
split/02-website-integration
branch
from
August 29, 2026 16:08
05ed829 to
284ada7
Compare
Deicyde
changed the title
Summary: Add reusable finite and Sierpinski constructions, formalize S1, S4, S10, and S189, and register their direct and generated derived property certificates with the Lean-native audit. Add deterministic scaffolding and trait generation plus the spaceAudit executable, yielding four complete pilot spaces and 86 audited certificates. Test Plan: - python3 scripts/gen_spaces.py --check - python3 scripts/gen_traits.py --check S1 S4 S10 S189 - lake build spaceAudit - lake env lean PiBaseLean/Audit/Spaces/Tests/ReportSmoke.lean Generated Files: Run meerkat after landing if repository-wide generated metadata requires refresh. Tags: stack_created_with_devmate
Summary: Move derived space certificates out of handwritten lemma files into complete generator-owned modules. Keep direct proofs reviewable, make stale checks cover the full generated module and its handwritten sibling, and update space scaffolding and aggregate imports for the three-file convention. Test Plan: - python3 -m unittest discover -s tests -p "test_*.py" - python3 scripts/gen_traits.py --check S1 S4 S10 S189 - python3 scripts/gen_spaces.py --check - lake build spaceAudit PiBaseLean.Audit.Spaces.Tests.ReportSmoke - lake exe spaceAudit Generated Files: Run meerkat after landing if repository-wide generated metadata requires refresh.
Summary: Replace Python source inspection with a thin consumer of the Lean spaceAudit JSON report, then expose kernel-audited presentation, certificate, assumption, and axiom status in the dashboard. Enforce generated freshness and audit success in CI and Pages using the checked-out commit as the sole Lean authority. Test Plan: - python3 -m unittest discover -s tests -p "test_*.py" - npm run dashboard:check - npm run dashboard:build - npm run dashboard:verify - npm run audit:run Tags: stack_created_with_devmate
Summary: Preserve the handwritten/generated source split in dashboard review payloads. Direct certificates and generated derived certificates are rendered as separate collapsed sections, and artifact verification rejects missing generated source. Test Plan: - npm run test:python - npm run dashboard:check - npm run dashboard:build - npm run dashboard:verify
Deicyde
force-pushed
the
split/02-website-integration
branch
from
September 1, 2026 00:21
284ada7 to
411b033
Compare
|
This is really good! Having the spaces alongside proofs that they have various asserted properties helps to ensure the properties are aligned with their human-readable descriptions. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Important
This PR is stacked on #1319 at its verified head
5053d2cc. Review the upper layer with the fork comparison.#1319 is green and mergeable, but the fork owner does not have upstream merge permission. After an upstream maintainer squash-merges #1319, this branch must be rebased onto that squash commit and force-pushed before this PR can merge; the GitHub diff against
masterwill not shrink automatically.Summary
S1,S4,S10, andS189) with 14 direct certificates and 72 generated consequences.spaceAuditexecutable and publish its fail-closed result through the dashboard and review UI.pibase-datarevision and every Action used by the changed CI/Pages workflows to immutable commits.Review guide
37f93e38— formalize the four pilot spaces and preserve the report-status regressions from Add a Lean-native registry for Pi-Base spaces #1319.d436c376— isolate generated certificate modules.b78de9ab— add the executable audit, dashboard projection, CI, and Pages publication.67d6e329— expose generated certificates in review data.f8c0a67a— harden Markdown rendering and review-data loading.bd3ad4f2— make published audit data fail closed against catalog contracts.385f6271— pin external inputs and split unprivileged build from privileged deploy.bf3dc7de— bind artifacts to a fresh audit and the exact generated certificate contract.5cea684b— remove the competing docgen Pages deployment from read-only CI.411b033c— pin changed workflow Actions to immutable commits.Validation
--wfail: 4,115 jobs, including the executable audit and all registry/report/duplicate smoke testsnpm run generated:checknpm run test:python(74 tests)npm run test:frontend(3 behavioral security/contract tests)npm run dashboard:checkgit diff --checknpm cireported 0 vulnerabilities; a standalone audit refresh was unavailable because the npm audit endpoint returned HTTP 503The PR remains draft until an upstream maintainer squash-merges #1319, this branch is rebased onto that squash commit, and CI is rerun.