Repository navigation
Forward merge release/v0.4 (0.4.0, e0b74b81) into release/v0.5 - #325
Closed
humuhumu33 wants to merge 78 commits into
Closed
humuhumu33 wants to merge 78 commits into
humuhumu33 wants to merge 78 commits into
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
…nt for the number functions, RustStd with 17 more functions and theorems (unpruned definitions), the number text as methods of Str (statements and counts to finish)
…into claude/issue-91-stage4-heap-h6
…454) The row, its scenario, its section-31 row and CONFORMANCE line, and the named case conformance_sp_30, which fails on this head: the compiler table of runtime items holds formatInt (the decimal text of an integer, called as format_i64), and no theorem of RustRuntime or RustStd states it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…ecimalInt SP-29: the number functions are parse_int, format_int, and the format_ and parse_ function of each fixed width, one machine call each; formatDecimalInt is the calculus primitive formatDecimal at the integers. RB-20: families 26 to 43; format_int, which the handwritten runtime called as format_i64, is held to the digest the transcript records for format_i64 on the same values; a format_int that formats at another width is refused. The SPEC, CONFORMANCE and feature copies of both statements are the ids.toml text byte for byte. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
SP-29 lists refines_format_int; the RB-20 harness calls format_int on the values of format_i64 and holds it to the recorded format_i64 digest (HELD_AS); SP-23 expects 44 machine constructors and BS-05 one more machine crate. Red until the next commit adds the function, the primitive, and the theorem. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
… refinement theorem The runtime item FormatInt (the decimal text of an integer) had no function of its own: the generated code called format_i64 for it, and no theorem stated it. RustSyntax gains Machine.formatDecimalInt (family 43, one operand, no width), whose meaning RustSemantics states as the calculus primitive formatDecimal, the same as Item.formatInt; RustStd defines format_int as one call of it, printed as Str::format_i64 because the printed runtime holds the integers as i64, with the theorem refines_format_int; Item::FormatInt is called as format_int. The bootstrap twin of RustValidate names family 43 and the item row format_int. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…5 counts RB-20: a format_int that formats another value keeps its own label, which the golden transcript lacks (HELD_AS), and the statement says so. The unit test every_item_exists_with_its_failure_mode looks up the free function at the start of a line: the number text has the method Str::parse_int, which the lookup took for parse_int. BS-05: the four families 40 to 43 add one vector each to the validate and correspond counts and to the evaluator counts (464/213, 327/100, 438/301), as the ten of H4b added ten. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…eorems; the index plant without overflow The shared term_cases list is pruned as H4b did: the 40 names H5 kept and the eighteen number-function definitions (58) prove every theorem but the eight format_<w> and parse_int; against format_i16 alone each of the 15 other names was dropped (allWidth and hasWidth are needed), and against parse_int alone (constructValue, evalArms and literal are needed); the 63 prove all 32. RB-20: the plant "an index that finds the next position" computed i + 1 at the harness index u64::MAX and panicked on the overflow without naming index_list, so the case failed on the accepted H5 head 45f2f07 as here; with wrapping_add the planted index returns the next item and the transcript names index_list. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…SP-30, and the figures Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…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
…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
… 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
…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
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
The first pass's check-fixtures ran with an xtask the shared build directory had taken from another worktree (its repository root is fixed at compile time) and stopped when that worktree went away, so the fixtures whose identity moved kept their old records; the first gate refused vr-11, vr-15, cl-04 and cl-05 on their source ids. 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
…ap-h6 Stage 4 heap half H6 on release/v0.4: register 458, regeneration on the H6 identity, Atlas records joined. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013QppGKetUURseXowZun9KY
Contributor
Author
|
Closing this in favour of the branch form the line has used for forward merges (#322, #245). Two reasons it cannot land as opened:
The forward merge is: a branch cut from |
Member
|
Agreed on both counts; that is the form in progress now. The second forward merge (H5 #298, the release-workflow fixes #320/#321/#323, and H6 #304, i.e. Generated by Claude Code |
Member
|
Please stop the parallel forward merge on The forward merge is complete on If you want to help here: review the PR when it opens, in particular the three-way resolutions in Generated by Claude Code |
Member
|
#327 is merged at Generated by Claude Code |
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.
Forward-merges the released v0.4.0 line into the v0.5 line, per the branch model of #15: a release X.Y lives on
release/vX.Y, is tagged there, and is merged forward into the next line after each landing.release/v0.4is ate0b74b81e6f49c83596a957d232c8383a5db1a25— thev0.4.0tag commit (run 40382770933, release published 2026-10-26T19:20:36Z). The earlier forward merge, #322, took93fbe7df9at 11:41Z, before the tag was moved offaa6593e0, so this line still lacks the released commits — including #323 (release-gate.sh ends the evidence with the line the release criterion reads) and #309 (the workspace version is 0.4.0).compare/release/v0.5...main: main is ahead by 47, behind by 128.