Skip to content

Fix compiler diagnostics and release-evidence validation - #403

Merged
afflom merged 8 commits into
release/v0.4from
fix/issue-377-policy-diagnostics
Nov 3, 2026
Merged

afflom merged 8 commits into
release/v0.4from
fix/issue-377-policy-diagnostics

Conversation

@afflom

@afflom afflom commented Nov 3, 2026 •

Copy link
Copy Markdown
Member

Deep authoring terms could abort, semantic JSON depth errors offered no remedy, and verification reported only the first axiom-policy failure at the project manifest. This maintenance integration fixes those diagnostics and a separately reproduced release-evidence pipe failure.

  • AU-03 enforces the existing depth-256 authoring bound for terms and types, including unclosed input, with positioned LLP2001 instead of a stack abort.
  • SM-12 retains the 128-level semantic JSON limit and reports smaller definitions joined by prim append as the remedy. The existing recursion-limit category is preserved for SP-02; generated JSON coordinates are not presented as authored-source positions. Deliberately refused fixtures use the existing negative/ classification; AU-08 is unchanged.
  • VR-11 collects every LLV7005 before publication and uses declaration source spans. Language-1.2 anchors reuse the existing Lean source-map entries, eliminating a redundant source parse; legacy v1 retains its existing lookup.
  • The release gate consumes complete jobs listings when matching required rows, preventing producer SIGPIPE under pipefail. Required legs, host count, tree matching and refusal of every failed job remain unchanged.
  • The workflow timeout comment records Reduce repeated host conformance work and bound scaling to Linux (#235) #400's measured Intel result: 117m01s versus 144m02s baseline, with all468 cases passing in6021.07s versus7470.84s. The timeout stays240 minutes. The optimization itself already landed in Reduce repeated host conformance work and bound scaling to Linux (#235) #400.

This replaces #401 and #406 with one reviewed final integration and one complete gate. Their exact published heads are preserved in this branch's merge history, along with all verification records. The branch now also includes the landed BS-20 release commit 0a01df6. No compiler identity input or generated oracle was changed.

Validation:

  • After the BS-20 base integration, formatting, model audits (469 IDs/86 codes), specification links and all five BDD meta-tests passed.
  • Exact RP-18, AU-03 and SM-12 passed on the combined implementation (1.09s,20.72s,1.88s).
  • AU-08 reproduced the misplaced negative-fixture failure, then passed its unchanged corpus walk after relocation (723.03s); SM-12 also passed afterward.
  • The release-gate large-list assertion fails before the fix and passes after it, retaining the late-failure refusal and every existing decision.
  • The final map-anchor refactor passed CLI build and all-target/all-feature Clippy. One direct pinned-Lean run returned the identical three LLV7005 diagnostics and exact declaration spans as before, with no artifacts published.
  • The prior integration at 39399a2 passed all 42 jobs in CI 41634793106 plus honesty and reproducibility. The final BS-20-integrated head passed all 43 jobs in CI 41658939956, honesty 41658939965 and reproducibility 41658939998. Neither the separately reproduced SIGPIPE defect nor the removed source reparse is claimed as the established cause of the previous head's ordinary RP-18 failure or TC-03 overflow. Those prior failures require final-head gate evidence.

Reviewed integration tree: 88d8b657f1ab621bf736b9d7e5d97fcb9c834e5e at head 215a9d5. Its parents preserve the prior maintenance head and landed release/v0.4 at 0a01df6; only the verification-record append conflicted, and both records remain intact.

Closes #374.
Closes #375.
Closes #377.
Closes #235.
Closes #408.

Landed as 5a44fe49e5d73569c3bb377bb28b56e463ee0547 on release/v0.4. Actual merge tree 88d8b657f1ab621bf736b9d7e5d97fcb9c834e5e equals the final reviewed/tested head and synthetic merge tree. Issues #374, #375, #377, #235 and #408 were explicitly closed with this evidence after landing.

afflom and others added 2 commits November 2, 2026 23:55
Enforce the existing depth bound in recursive readable terms and types.
Cover 50,000-level closed and unclosed input through the API and CLI,
exact readable boundaries, and independent guard-removal plants.

Closes #374.

afflom commented Nov 3, 2026

Copy link
Copy Markdown
Member Author

I’m investigating the failed honesty job on c055e4a and will keep the gate intact. I’ll post the focused reproduction and correction once checked.

afflom commented Nov 3, 2026

Copy link
Copy Markdown
Member Author

Fixed the honesty failure in 519694d: VR-11 had eight steps against the Gherkin subset’s six-step bound. Consolidated related outcomes into six steps, preserving every expectation and leaving the gate intact. Reproduced the original failure locally; all five bdd meta-tests (including planted-defect falsifiability), validate-model, and diff checks now pass. The published tree equals the locally reviewed 5749680e4 tree byte for byte.

Run 41605700263 passed the full bdd-verification leg on the original implementation, including VR-11. A separate blocker remains: bdd-compiler job 125815139388 aborted with a stack overflow in conformance_tc_03. The ARM, Windows, and rest failures inspected were the same eight-step honesty failure corrected here. No old jobs were manually rerun; the new head supplies fresh CI evidence.

Retain the 128-level reader bound and recursion-limit category, explain smaller definitions joined by prim append, and cover the boundary and validation refusals.

Closes #375.
Retain both VERIFICATION records after their append-only conflict. Model, specification links, formatting and diff checks pass on the resolved tree.
Comment only: retain the 240-minute timeout and every workflow token.

Closes #235.

afflom commented Nov 3, 2026

Copy link
Copy Markdown
Member Author

Maintainer coordination: I am preparing one combined maintenance integration from this head plus the existing #401 and #406 heads, preserving their histories and reviews. #401's complete gate is green but its verification-record appendix conflicts with the updated release line; #406 needs its intentionally refused fixtures classified under the existing negative-input convention. The repeated TC-03 overflow and RP-18 failure are being investigated separately, with no acceptance checks disabled.

The combined, reviewed final tree will run one complete gate before landing, avoiding three separate full matrices after these integrations. Its final description will name the precise issue closures (#377, #374, #375 and #235); the original PRs stay open until their source is incorporated and reviewable. No identity regeneration is part of this maintenance integration.

Combine authoring depth refusal, complete policy diagnostics, semantic JSON nesting advice, negative fixture classification and release-gate listing consumption. Reuse rendered semantic mappings for policy source anchors. Preserve both feature histories and verification records.

Tree matches reviewed local integration 0cfb8c4f48e17945cdab7ae5d5a4757d05cfb594 exactly. Final-head acceptance CI remains required.
@afflom afflom changed the title verify: report all axiom-policy failures at declaration spans Fix compiler diagnostics and release-evidence validation Nov 3, 2026

@afflom afflom left a comment

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Reviewed the final combined tree411f68fa973103b1e1d03e6cff0dae2ae75ead6b, including independent Sol 6.1 reviews and focused validation. Exact published parents preserve all source from #401/#406. Appendix resolutions retain every record; the fixture correction preserves bytes and AU-08's existing invariant; the release-gate change preserves every acceptance predicate; semantic policy anchors reuse already-rendered Lean mappings in declaration order. No identity regeneration or acceptance exemption was introduced.

Source review is clear, conditional on the complete final-head gate. Do not merge or close #374/#375/#377/#235/#408 while any required result is incomplete or failing. The earlier TC-03 and ordinary RP-18 failures have not been assigned a proven cause; this review does not relabel them as infrastructure failures or authorize blind reruns.

Preserve both verification appendices and carry the already-tested BS-20 generated artifacts unchanged. No source conflict or regeneration.

afflom commented Nov 3, 2026

Copy link
Copy Markdown
Member Author

#364 has now landed as 0a01df6 after all 43 jobs passed. This advances release/v0.4, so the current run here remains evidence for the old integration tree, not final merge clearance against the new base.

I prepared the updated merge locally as 215a9d5 (tree 88d8b657f1ab621bf736b9d7e5d97fcb9c834e5e), preserving exact parents 39399a2 and 0a01df6. Only the VERIFICATION append conflicted; both records survive. All source-only blobs from both sides are preserved; shared source/model deltas retain their reviewed patches. Formatting, model audits (469 IDs/86 codes), spec links and all five BDD meta-tests pass on the correctly rooted local tree. No identity inputs or generated oracles changed relative to the new base.

The remote branch is deliberately unchanged while CI 41634793106 finishes. I will publish the reviewed integration afterward and require complete final-tree evidence before merge. Please avoid a duplicate base-merge patch or using the old-tree checks as new-tree acceptance. #413 remains a separate stacked optimization pending this landing.

@afflom afflom left a comment

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Reviewed the BS-20 release-base integration at tree 88d8b657f1ab621bf736b9d7e5d97fcb9c834e5e. All BS-20-only and maintenance-only source blobs retain their parent contents; shared source/model changes retain the reviewed patches. Only the VERIFICATION append conflicted, and both records survive. No identity input or generated artifact changed relative to the landed release base. Correctly rooted formatting/model (469 IDs, 86 codes)/spec links and all five BDD meta-tests pass.

The previous maintenance tree passed the complete 42-job gate 41634793106, honesty and reproducibility before this integration was published. That establishes the old tree, not this one. Source review is clear, but merge and closure of #374/#375/#377/#235/#408 still require complete new-head CI and actual merge-tree equality. This is a source review COMMENT on a self-authored PR, not self-approval.

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