[humuhumu33]

Refs #34. Draft: it lands last, after the whole stack, in the order afflom places it.

The workspace version goes from 0.3.0 to 0.4.0, so a v0.4.0 tag passes the check in release.yml that refuses a tag whose version differs from Cargo.toml.

Every site changed

Site	Change
Cargo.toml	[workspace.package] version, and the three internal requirements repo-model, repo-conformance, lexlean
Cargo.lock	lexlean, repo-conformance, repo-model, xtask
SPEC.md §2.3	the [workspace.package] block
crates/conformance/src/cases/repository.rs	RP-01 (the version = "0.4.0" row and lexlean 0.4.0 on --version), the RP-12 failure message
CHANGELOG.md	## Unreleased becomes ## 0.4.0, as ## 0.3.0 was recorded; the intro clause "Unreleased holds what has landed since" names 0.4.0
25 expected/build/manifest.json	compiler.version; build_id does not include the version, so no other byte of them moves
tests/fixtures/cli-api/cl-05-build-artifacts/expected, tests/fixtures/verification/vr-11-exact-success/expected	the two fixture records that hash those manifests

The records come from cargo xtask check-golden --write and check-fixtures --write (27 files changed); both check commands are clean afterwards. No workflow changes: release.yml and crate.yml read the version from Cargo.toml, and no lock or register row derives from it.

Left as they are

• VERIFICATION.md receipts for Release Closure: Complete LexLean artifacts/oracle evidence required by PrismPM 0.3.0 acceptance #2, Release Identity: Deliver LexLean artifact/provenance package required by PrismPM v0.3.0 acceptance #3 and Publishing Bootstrap: Close first-party package identity and initial upload requirements #5 name 0.3.0 and the digests of that crate: they record what was verified at 0.3.0.
• SPEC.md "the untagged 0.3.0 API" and the ## 0.3.0 CHANGELOG section: history.
• xtask/src/release_manifest.rs unit tests: 0.3.0 is a literal input there, not the workspace version.
• The CHANGELOG intro still says "Only v0.1.0 has been tagged": that sentence is the maintainer's to change when the tag is cut.

Checks (local, WSL)

On the head 3971b2771 (merged with the line at fbfaa73fe, register 453): cargo fmt --all -- --check, validate-model (453), validate-spec-links (453), check-test-inventory (792), check-golden, check-fixtures (304) clean; conformance_rp_01, conformance_rp_12 and conformance_cl_24 pass.

cargo xtask release-check (run on the tree before the merge of #261): the packaged crate builds standalone and prints lexlean 0.4.0, language 1.0, compiler-semantics 430ba0a3e1b8565688b38dfaf7e1f3422576dc603349e7574ab56fe4d9e14541 (this moves with every identity landing still to come), lean-toolchain leanprover/lean4:v4.32.1. It then refuses, as it must before 1.0.0, naming source-tag twice (the version is not 1.0.0; no ## 1.0.0 entry) and the artifacts the release workflow derives and a checkout does not hold (checksums, five host-binaries, crate-package, semantics-id, version-output, sbom, ci-evidence). release.yml allows exactly source-tag and version-output to be unmet and generates the rest before it runs the check, so nothing here is new.

Not verified: a release.yml run (needs the maintainer's go-ahead on #34) and the full CI gate, which this draft only runs in its rest leg until it is marked ready.

Keeping it current

The branch is merged forward after each landing on release/v0.4 (merge commit, register count at every site, no rewrite).

🤖 Generated with Claude Code

[humuhumu33]

Head 2e9033c1a: release/v0.4 at 18de05031 (#265 landed) merged in, one merge commit, no conflicts; the register is 454 at every site (the bump changes no count). #265 added no record that still names 0.3.0. Local: fmt clean, validate-model 454, validate-spec-links 454, check-golden and check-fixtures (304) clean, conformance_rp_01 and conformance_rp_12 pass. Still a draft; I merge the line forward again after each landing.

---

Generated by Claude Code

[humuhumu33]

Head 915bbd524: release/v0.4 at 201519a1b (#293 and #297 landed, identity moved, register 456) merged in at 3e84aa2ac. The 27 files the line regenerated on the new identity (25 build manifests, two fixture records) conflicted with the version change, so they were taken from the line and rewritten for 0.4.0 in the next commit with check-golden --write and check-fixtures --write; every manifest differs from the line's only in "version". Register 456 at every site. Local: fmt clean, validate-model 456, validate-spec-links 456, check-test-inventory 795, check-golden and check-fixtures (304) clean, conformance_rp_01 and conformance_rp_12 pass. Still a draft.

---

Generated by Claude Code

[afflom]

Maintainer: this PR is the v0.4.0 tag commit, per the owner's ruling on #92 (6399822402, 6399888863): the release is cut at the downstream boundary, release/v0.4 as it stands plus this bump. I pushed one commit onto the branch, 4d6cb40b0 (CHANGELOG.md only): the intro sentence now says v0.1.0 is tagged and v0.4.0 is tagged at this commit, and the 0.4.0 section opens with the release paragraph the #34 ruling requires: the cut, the register (456), the three compiler-semantics IDs, and exactly which bootstrap (BS-01 to BS-06, BS-09) and runtime-as-source (RB-15 to RB-17, RB-19, RB-20, SP-21 to SP-23, SP-25 to SP-29) stages ship, with the rest named as 0.4.1 and 0.5.0 material. The head at 915bbd524 already contained the line (201519a1b) and was mergeable. Marked ready; the full gate runs on 4d6cb40b0; I merge on green, then the release.yml rehearsal, the tag, main receives the line, and release/v0.4 forward-merges into release/v0.5.

---

Generated by Claude Code