Repository navigation
main receives the v0.4.0 line: release/v0.4 at e0b74b81e (the tag) - #324
Merged
Merged
Conversation
…ster statements, SPEC.md rows, and the failing named tests The std runtime's types, impls, and helpers become a second module, RuntimeStd; RB-20 states it, RB-19 states the associated function the validator learns for it, BS-09 the two plants that follow (648 crates). The tests are red: the module is not shipped, and the validator and its Lean twin refuse the associated call only by name.
…ociated-call rule and its twin, the printer's compound assignment, the library table
…s records what a call returned and counted, the handwritten runtime and the printed one agree on them, and the golden transcripts are recorded (the last pass of the differential)
…rated at landing)
…ow, the SPEC.md row and paragraph, the scenario, the failing named test; RB-16, RB-17, RB-20 state the golden transcripts; the register order of RB-20 and two stale ranges
…ed, the cases compare the golden transcripts, and nothing holds runtime text but the printed modules
… into claude/issue-91-stage4-heap-h5
…--write, a changed-byte plant, and the statements say the comparison is against a recorded transcript of the removed oracle
…ranscript, its writer, and the red lines of the plants
…nts, the one transcript file named, the old counts, the module doc of runtime.rs, the unreachable decimal branch dropped, the decimal text's history and the largest module's Lean time
…overflow at u64::MAX (wrapping_add), so the transcript names index_list
…ed; statement, SPEC §17.23, CHANGELOG Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018vK7Tm6xHF5etAwKM6r9HG
Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018vK7Tm6xHF5etAwKM6r9HG
…mantics identity; locks, goldens, calculus, packages, fixtures and provenance regenerated Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013QppGKetUURseXowZun9KY
…but the Atlas, on the moved identity Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013QppGKetUURseXowZun9KY
…een shard artifacts of the first gate run Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013QppGKetUURseXowZun9KY
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013QppGKetUURseXowZun9KY
The case checked that the scan read the runtime sources by comparing each repo-relative path with a forward-slash literal; on Windows the stripped path carries backslashes, so the first gate on x86_64-pc-windows-msvc failed with "the scan reads crates/lexlean/src/calculus/rust/runtime.rs" while the scan had read it. Normalising the separator is what the other cases that show paths already do. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013QppGKetUURseXowZun9KY
…mit, not a second run of the gate on one runner Rehearsals 3 and 4 showed the `just vv (release evidence)` job cannot finish: the `bdd` recipe alone took over four hours on one hosted runner and the job reached the six-hour limit before Atlas, so a tag would fail there and `image`, `manifest`, and `publish` all wait for it. The CI evidence §30.3 asks for already exists: `ci.yml` runs the whole gate as the parts of one run on every push to the line. `.github/release-gate.sh` finds the run that was the whole gate on the commit's tree (the commit, or the second parent of a merge that lands its tree unchanged, as `ci-plan.sh` reads a push), requires every job of it to have passed with the Atlas join, every host, and every leg present, and writes `vv-evidence.txt` with the run, its jobs, and the legs' retained transcripts. SPEC §9.4 and §30.3 say so; `conformance_rp_18` requires the gate job to run the script and no recipe, plants both, and runs the script against planted runs. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013QppGKetUURseXowZun9KY
…every conclusion refuses it Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013QppGKetUURseXowZun9KY
…ry leg refuses it Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013QppGKetUURseXowZun9KY
…t (RP-18, #34), with its plants Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013QppGKetUURseXowZun9KY
…ap-h5 H5: the heap half's fifth landing on release/v0.4, with its Atlas records and the RB-21 path-separator fix. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013QppGKetUURseXowZun9KY
…e branch Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013QppGKetUURseXowZun9KY
The release's evidence is the gate run of the tagged commit, not a second run of the gate on one runner. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013QppGKetUURseXowZun9KY
…ixes that reached the line while the tag waited The register is 457 and the three compiler-semantics IDs are the ones the locks pin after H5; RB-21 ships; the std runtime types, impls and helpers are in (RB-20), the number functions and the lowering stay 0.4.1. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013QppGKetUURseXowZun9KY
…inement theorems; H5 printed their text Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013QppGKetUURseXowZun9KY
The 0.4.0 cut carries H5 and the release-workflow fixes; this is the v0.4.0 tag commit. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013QppGKetUURseXowZun9KY
… reads The first v0.4.0 tag run passed every job but `publish the release`, which stopped at release-check: the §30.3 criterion reads the line `just vv` prints when the whole gate passes, and the file the release gate writes from the sharded run carried the run, its jobs and the legs' transcripts, none of which says it. The rehearsals could not show this, since `publish` runs on a tag only. The script now ends the file with `gate: every job of run N passed on <commit>` and `vv: the acceptance gate passed`, the criterion is one function (`repo_model::release::ci_evidence`) with its own test, and RP-18's planted-run test holds the script's output to that function. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013QppGKetUURseXowZun9KY
release-gate.sh ends the evidence with the line the release criterion reads; this is the v0.4.0 tag commit. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013QppGKetUURseXowZun9KY
This branch was successfully deployed
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
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.
What
mainreceives therelease/v0.4line at its tag, as the release-lines rule of 2026-10-20 says (SPEC.md §9.4,RP-14). The line's heade0b74b81e6f49c83596a957d232c8383a5db1a25(merge of #323) is the commit thev0.4.0tag now names: the 0.4.0 release notes, the H5 landing (#298), and the release-workflow fixes (#320, #321, #323).maincarries only the merge commit of #319 beyond the line, so this is the line's own history plus that merge; a direct push tomainis declined by the repository rules, hence the pull request.Evidence
The tag's release run 40382770933 passed every job including
publish the release; the GitHub release andlexlean 0.4.0on crates.io were produced from this commit. Every commit on the line landed through a green full gate on its own pull request. No file changes beyond what the line carries.Generated by Claude Code