Skip to content

Repair 4.0.1 fixture correspondence and require Lean 4.35.0 - #143

Merged
docxology merged 1 commit into
mainfrom
codex/native-fixture-release-repair
Oct 15, 2026
Merged

docxology merged 1 commit into
mainfrom
codex/native-fixture-release-repair

Conversation

@docxology

@docxology docxology commented Oct 15, 2026 •

Copy link
Copy Markdown
Owner

Prepared fixture bodies intentionally remain untracked, but native mirror correspondence indexed them as committed Git blobs and failed before format execution. Authenticate their complete manifest census and declared modes while retaining committed-file mode authority, byte correspondence, and refusal of hidden or undeclared bodies. Five genuine Git/fixture cases cover the successful path and four failure modes.

Integrate the intended Lean 4.35.0 release changes across both public Lean exemplars and CI. Exact-version admission rejects older and lookalike pins; the Active default Lake target elaborates its library. Canonical Active regeneration exposed runtime setuptools metadata entering its semantic source fingerprint; exclude only direct src/*.egg-info directories after the existing symlink refusal, with real filesystem regressions for metadata stability and authored-input binding.

Validation:

  • 36 fixture/preparation tests, 19 direct Lean controls, and 9 focused fingerprint tests passed. Both genuine Lean builds and all 24 axiom audits passed; Formal TLC positives and required negative control passed.
  • Exact project coverage measurements: Active 91.41%, Formal 90.37%. Active uses the declared release profile, including one empty-selection slice; no runtime pass count is inferred from discovery.
  • Full public Ruff/format and mypy passed; counts regeneration and consistency check passed.
  • The independently reviewed policy preserves all 29 obligations and all 12,172 prior classifications; adds one five-case family with its Git prerequisite.
  • All 25 public output validations passed; the strict staged rendered-publication audit found zero findings. Seven Active semantic/audit reports were canonically regenerated; manuscript text, variables, figures and rendered deliverables remained byte-identical.
  • All 26 wheels passed exact-source admission on committed candidate b3e9ea8528557d4cc60c970962c579573d84fa62. Fresh original census/plan admission authenticated 12,173 families, 14,911 nodeids and all 29 obligations with source unchanged; policy SHA256 8230a75700eded116eb05d59e9b01aad16fc500c934bf460dd05f7118c22b79a. These are source/census checks, not native runtime acceptance.

This development repair prepares 4.0.1. The previous hosted acceptance run failed and cannot authorize publication of this source. After merge, fresh exact-main hosted required acceptance and its authenticated release handoff remain required before v4.0.1 is tagged and published.

@docxology
docxology merged commit 36a4d12 into main Oct 15, 2026
33 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant