[afflom]

Closes #257 (milestone v0.4, so this targets release/v0.4 per AGENTS.md "Release lines").

What

lexlean migrate --to 1.2 [--check] migrates a language-1.1 data-form project, path lexicon packages included, to language 1.2 in one command:

• every module is rewritten from \semanticdata{...} to the authoring notation through lexlean::sdk::to_notation (tag /1 to /2 first), and the notation must read back to exactly the module, so declaration names, theorem statements and axiom policies are unchanged;
• builtin glossary references move 1.1.0 to 1.2.0 in every \useglossary and in each path lexicon manifest's imports; the manifest language becomes 1.2 (entries and package version untouched);
• the language row is rewritten (canonical lexlean.toml) and the lock regenerated as lexlean/lock/2.

The migrated project is first written into a scratch copy, locked and checked as language 1.2. Only then are files staged and renamed together (rollback if a rename fails). The mutation lock is taken after the proof, so a refusal writes nothing and creates no .lexlean. Refusals: LLC0103 (project not language 1.1), LLP2003 (not a 1.1 data-form semantic module, or no notation), or the scratch check's own diagnostics. --check runs the same proof and writes nothing.

Engine keeps its seven entry points (CL-13); the function is lexlean::api::migrate::migrate. No new diagnostic codes.

Register / spec (R3)

• CL-24 row in model/ids.toml + SPEC §31 table (§17.12, §23.4), scenario in features/suites/cli-api.feature, test conformance_cl_24 (cases/migration.rs): --check writes nothing; full migration of examples/semantic-1.1 plus a language-1.1 path lexicon package (modules read back equal under the 1.2 tag, check, lock --check, fmt --check pass); a migrated project and examples/language-1.2 refused with LLC0103; --to 1.1 refused; every refusal leaves all files byte-identical.
• Negative fixture tests/negative/migrate-module-without-notation (LLP2003).
• SPEC §17.12's stale recipe replaced; §23.4 documents migrate. Register count 436 to 437 (RP-07 constant, SPEC total, README, CHANGELOG, regenerated CONFORMANCE.md).

Verification

Locally (no Lean toolchain on this host): cargo fmt --check, cargo clippy --all-targets --all-features -D warnings (lexlean, repo-conformance, xtask), xtask validate-model, validate-spec-links, check-test-inventory, conformance_cl_24, the bdd meta-gate. Not run here: the Lean-backed cases and just vv; CI owns those.

Real project: a copy of the prism-code model (9 data-form modules + prism.arch path lexicon, language 1.1) migrates with lexlean migrate --to 1.2; the copy then passes lock --check, fmt --check --all, check --all and build --all. verify needs the pinned Lean toolchain, which is not installed on this host.

---

Generated by Claude Code

[afflom]

Pushed the reader fix for the nested-match case reported from the PrismPM SDK stdlib (keyword followed by { in a parenthesised term). Regression test is the unit test a_keyword_kind_written_generically_reads_back_in_parentheses.

---

Generated by Claude Code

[afflom]

CI is green on 0d1351d. Three follow-up fixes went in after the first run:

• EX-07 now lists the new negative fixture.
• RP-07 counts §31 at 437 rows, for CL-24.
• The prescribed-classes array length went from 285 to 286.

This is ready for review by the LexLean maintainers.

One note from using it downstream (PrismPM #224): migrate writes a match on a binder that collides with a keyword (first) in its generic match{...} form inside an infix operand. Readers before this PR's surface/semantic.rs fix refuse that with LLP2001, so a v0.4 build is needed to read migrated output back.

---

Generated by Claude Code

[humuhumu33]

Review of 0d1351db5 (read from the diff; nothing built or run here).

The main path is sound. The round-trip proof compares the whole module value (migrate.rs:154), so a mismatch can only produce a false refusal, never a silent change. The lock is taken after the proof (:373 before :385), so a refusal and --check write nothing into the project. The register is 437 in all four places plus ids.toml. EX-07 lists 286 entries, matching the 286 fixtures.

Two items before merge, three test gaps, and a rebase.

Before merge

1. Rollback stops at the first failed restore (crates/lexlean/src/api/migrate.rs:343). In publish, a failed persist restores the published files in reverse, but the ? on each restore returns at the first one that fails. Every file not yet restored stays migrated. On Windows, a module held open by an editor or a scanner is enough to trigger it. The result is a project that is partly 1.1 and partly 1.2, and the error names only one path. This contradicts the doc comment "the project is never left half migrated". Suggest attempting every restore and reporting all the failures together, plus one case that forces a publish failure.
2. The LLP2003 fixture is not a valid language-1.1 module. tests/negative/migrate-module-without-notation/project/src/Main.lex.tex carries "note":"kept". schemas/semantic-module.schema.json forbids that, because the top level is additionalProperties: false with only declarations and spec. So the claim "a module the notation cannot express is refused with LLP2003" is tested only on malformed input. Either use a schema-valid module the notation cannot express, or reword the claim to what is tested.

Test gaps

3. The reader-fix test does not reach the changed lines (surface/semantic.rs fix at about :1300, test a_keyword_kind_written_generically_reads_back_in_parentheses at about :1937). All three inputs print as (true && kw{…}), so the generic node is the right operand. That operand is read by terms::read (about :1168), which already accepted kw{. Only a generic keyword node first after ( reaches the new guard, and I believe this test passes on the base branch too. Separately, the guard also turns hand-written (let {name: x, type: …} := v; b) into an error. That form read before this PR, but the printer does not emit it, so the impact is low.

4. Claims in §23.4 that conformance_cl_24 does not test:

   • refusal when the scratch copy fails its 1.2 check;
   • LLC0103 on a path lexicon manifest;
   • LLP2003 on a non-semantic module;
   • "the files are then replaced together".

   The "--check creates no build root" assertion is vacuous as written: add_path_lexicon calls relock() (migration.rs:50), which creates .lexlean/.lock before the --check snapshot is taken.

5. The proof reads the project unlocked (:373 vs :385). stage re-reads each original under the lock but does not compare it with the bytes that were proven. A fmt or an editor save landing between the proof and the lock would be overwritten by text derived from the stale file. This is unlikely in practice; hashing the inputs in rewrites and re-checking them under the lock would close it.

Rebase. The PR conflicts with release/v0.4, which has gained 84 commits since cee0fbade, #248 among them. These files changed on both sides:

• CONFORMANCE.md, README.md, SPEC.md, model/ids.toml;
• crates/conformance/src/cases/{examples,mod,repository}.rs and crates/conformance/tests/conformance.rs;
• xtask/src/spec_links.rs.

Release is now at register 443 and EX-07 at 297, so after the rebase CL-24 makes them 444 and 298, in all four count places.

[afflom]

Addressed in 2efac77a6..4bf7b3a39 (pushed, no force). Merged release/v0.4 rather than rebasing.

Review item	Commit	Result
Merge with release/v0.4 (5 conflicted files, all counts)	2efac77a6	Register 444, EX-07 298 in README, SPEC section 31 total, spec_links.rs, repository.rs, examples.rs, CHANGELOG. validate-model reports 444 ids and validate-spec-links 444 rows bijective.
1. Rollback stops at the first failed restore	4bf7b3a39	rollback() attempts every restore and returns all failures; publish() reports them together with the persist error. Tests: forced publish failure restores every file; two unrestorable files around a restorable one are both reported and the middle one is still restored.
2. LLP2003 fixture is not a valid 1.1 module	1262fc169	I looked for a schema-valid module the notation cannot express and found none: the printer is total, strings with control characters, NUL and non-BMP code points all read back equal, and the serde_json recursion limit (128) refuses deep nesting before the notation's 256. So I took your second option: the CL-24 statement (ids.toml, SPEC section 31, feature, regenerated CONFORMANCE.md), SPEC 17.12 and 23.4 now say "a module that is not a language-1.1 data-form semantic module", and the read-back check is described as a guard. The fixture stays, as the payload the notation cannot spell that AU-04 asks of a refused fixture.
3. Reader-fix test does not reach the guard	86a8331cf	New test puts a generic not{..} / first{..} as the left operand, which prints (not{..} && true) and reaches the guard in paren(). It fails with the guard reverted and passes with it. The guard also no longer breaks hand-written (let {name: x, type: T} := v; b) (kept when the first member is name), with a test.
4. CL-24 / section 23.4 untested claims and vacuous assertion	61dba29b2	add_path_lexicon removes the build root its relock created; build-root presence is asserted around --check and every refusal. Added: files replaced together (changed set is exactly modules, manifest, config, lock), LLC0103 on a language-1.2 path manifest (migrate and --check), LLP2003 on a tooling module, refusal when the scratch copy fails its 1.2 check (unresolvable import, LLR3001; migrate and --check).
5. Proof/lock race	4bf7b3a39	rewrites() fingerprints (SHA-256 of raw bytes) every module, manifest and the config it read; stage() re-reads each under the lock and refuses with LLV7010 when the file changed or vanished, writing nothing. Tests: edit between rewrites and write is refused and survives; unchanged control; vanished original. SPEC 23.4 and CHANGELOG state it.

Checks run: cargo fmt --all -- --check; cargo clippy -p lexlean -p repo-conformance -p xtask --all-targets --all-features -- -D warnings clean; cargo test -p lexlean --lib 218 passed; conformance_cl_24, conformance_ex_07, conformance_rp_07 and the bdd meta-gate pass; cargo xtask validate-model and validate-spec-links clean. The full just vv (golden, repro, examples, deny) was not run here.

Not changed: the configuration file's fingerprint is taken when rewrites reads it, slightly after Engine::load, so an edit to lexlean.toml in that instant is not caught.

---

Generated by Claude Code

[humuhumu33]

Review of 4bf7b3a39, built and run. Not approving yet: the head does not contain release/v0.4, and two documented claims do not match the code. The migration itself did everything #257 asks on three real projects, verify included.

Host. WSL Ubuntu 26.04 x86-64, 12 cores, 15 GB. Rust 1.97.1, Lean 4.32.1 through elan. Debug build of lexlean at 4bf7b3a39. PrismPM projects from PrismPM main @ c1432003, copied, never edited in place.

Evidence: three language-1.1 data-form projects

Project	Modules, path lexicons	1.1 check, lock --check, fmt --check	migrate --check	migrate	1.2 check --all, lock --check, fmt --check --all	fmt --all after	migrate again (and --check)	1.2 build --all	verify --all 1.1 → 1.2
LexLean examples/semantic-1.1 (the only 1.1 example)	11, 0	pass	exit 0, tree byte-identical, no .lexlean	exit 0, 13 files changed	pass	byte-identical	exit 2 LLC0103, tree unchanged	pass	pass → pass (11 modules)
PrismPM examples/Calculator	1, 0	pass after lexlean lock (see note)	exit 0, unchanged, no .lexlean	exit 0, 3 files changed	pass	byte-identical	exit 2 LLC0103, unchanged	pass	pass → pass (1 module)
PrismPM tests/fixtures/holo/ho-11-text-application/project	4, 1 (prism.arch)	pass after lexlean lock	exit 0, unchanged, no .lexlean	exit 0, 7 files changed	pass	byte-identical	exit 2 LLC0103, unchanged	pass	pass → pass (4 modules)

After migration no \semanticdata and no @1.1.0 remain. lexlean.toml changes only its language row. The prism.arch manifest changes only language and its three imports (lexlean.core, lexlean.std.bool, lexlean.std.nat to 1.2.0).

Note on the baseline: both PrismPM locks are stale for this build (LLC0102, compiler semantics moved, because PrismPM main pins an older LexLean). The 1.1 baseline is therefore after a 1.1 lexlean lock. Migrating the stale-lock copy directly gives byte-identical output to migrating the relocked copy, for all three projects.

Evidence: refusals and edge cases

Case	1.1 check	migrate --to 1.2	Files unchanged	Build root created
Already 1.2 (examples/language-1.2)	pass	exit 2 LLC0103	yes	no
Language 1.0 (examples/nat-add-zero)	pass	exit 2 LLC0103	yes	no
Hand-broken data form (JSON truncated)	LLP2003	exit 1 LLP2003	yes	no
Data form carrying the /2 tag in a 1.1 project	LLT4001	exit 1 LLP2003	yes	no
A notation module inside a 1.1 project	LLR3001	exit 2 LLC0103	yes	no
Hand-edited data form, valid JSON, pretty-printed and keys reordered	LLT4001 "semantic-module JSON is not canonical"	exit 0, migrated	no, migrated	n/a (it migrated)
--to 1.1	n/a	exit 2 LLC0001	yes	no

No panic in any run. The reformatted module migrates to output byte-identical to the canonical example's migration, so no meaning changes. The issue is the documentation, item 3 below.

Before merge

1. The head does not contain release/v0.4. It is 20 commits behind (f057b8308, #254). A local merge conflicts in CHANGELOG.md, README.md, SPEC.md, crates/conformance/src/cases/repository.rs and xtask/src/spec_links.rs, so the register count moves again in all four places.
2. A stale-proof refusal creates the build root (crates/lexlean/src/api/migrate.rs:467). write calls acquire_lock, which runs create_dir_all on the build root, before stage (:470) refuses with LLV7010. SPEC §23.4 (SPEC.md:8965) says "a refusal writes nothing and creates no build root". Found by reading. a_file_changed_after_the_proof_is_refused_and_nothing_is_written checks file bytes but not the build root. Either remove a build root the call created on that refusal, or narrow the sentence to the refusals before the lock.
3. A non-canonical data form is migrated, not refused (migrate.rs:142). sdk::read_module accepts any JSON value, so a module that 1.1 check refuses as non-canonical (LLT4001) migrates with exit 0. That is a reasonable behaviour, because the read-back check still compares the whole value. But §17.12 (SPEC.md:4127), §23.4 and the CL-24 statement say a module that is not a language-1.1 data-form semantic module is refused with LLP2003, and nothing tests this case. Either refuse it with LLP2003, or state that migrate canonicalizes the data form and add the case to migration.rs.

Test coverage

• Covered by conformance_cl_24 and the unit tests: --check writes nothing; a whole migration with a path lexicon; read-back equality per module; check, lock --check and fmt --check after; second run refused; a 1.2 project refused; a non-semantic module; a 1.2 manifest; a scratch-check failure; --to 1.1; the rollback and the stale proof.
• Not covered: the notation-module branch (migrate.rs:133), the non-canonical data form (item 3), and build/verify of a migrated project. The table above gives the verify evidence that #257's definition of done asks for.

Docs

§17.12 and §23.4 state the command and its refusals. The README capability row names migrate and CL-24. CHANGELOG has the entry. Only items 2 and 3 above differ from the code.

[afflom]

Addressed at a9db189 (merge c709f46):

1. release/v0.4: merged into the branch at c709f46 (merge commit, no rebase). Conflicts kept both sides; the register count is 446 in README.md, SPEC.md, repository.rs and spec_links.rs, and validate-model/validate-spec-links pass.
2. Build root on refusal: write records whether the build root existed before taking the lock and removes the lock file and directory it created on any refusal after that point; a pre-existing build root is kept. a_file_changed_after_the_proof_is_refused_and_nothing_is_written now asserts the build root is absent, and a_refusal_keeps_a_build_root_that_was_already_there covers the other case.
3. Non-canonical data form: refused with LLP2003, using the same comparison 1.1 makes (whitespace atoms outside JSON strings dropped, the rest byte-equal to its canonical JSON), so laid-out sources still migrate. CL-24 has a case with a pretty-printed module and an escaped member name: 1.1 check gives LLT4001, and migrate and --check give LLP2003 with the tree and build root untouched. SPEC 17.12/23.4, CL-24 and the CHANGELOG say so.

Local: fmt, clippy -D warnings, validate-model, validate-spec-links, and cargo test --workspace --exclude repo-conformance --all-features pass; conformance_cl_24 and conformance_rp_07 pass. Golden, examples and the full bdd run are left to CI.

---

Generated by Claude Code

[afflom]

Maintainer review of a9db18930 (read from the diff, nothing built). The code is accepted; one small round before the landing.

Should fix

1. The fixture's lock is stale. tests/negative/migrate-module-without-notation/project/lexlean.lock:3 pins compiler_semantics = "176453256c…"; every other language-1.1 fixture and examples/semantic-1.1 pin 07965de9ea… at the merge base. It is harmless today, because migrate refuses at rewrites() before any lock is read, so EX-07 passes, but the fixture is not the valid-except-for-its-module 1.1 project its statement claims. Run lexlean lock in the fixture, or copy the lock header from model-under-1.1.
2. The merge with release/v0.4. git merge-tree conflicts in exactly four files, all the register count (README.md:150, SPEC.md "Total required capability IDs", cases/repository.rs:766, xtask/src/spec_links.rs:68-69); CHANGELOG.md:39 auto-merges but must say the merged size too. Nothing else in the PR depends on the count (EX-07's 298 is 297+1 on both sides). #91 stage 4, H1: RuntimeSyntax grows by the heap constructs — the probe module (RB-19) #255 is landing now and takes the register to 448, so this PR's merged size is 449. Leave the merge to me at the landing unless you push it first; if you do, merge commit, no rebase, counts 449 after #91 stage 4, H1: RuntimeSyntax grows by the heap constructs — the probe module (RB-19) #255 is on the line.

Nit: surface/semantic.rs:1301-1307, a malformed generic let{name: …} node now reads as a let with a binder and fails at :=; only an invalid node reaches it, a one-line comment would do.

What checked out: the round trip compares the whole module value with the tag flipped to /2 before to_notation; every LLC0103/LLP2003 refusal is in rewrites() before prove() and before the lock; --check returns before any write; the lock is taken after the proof; the build root is removed only when this run created it (tested); the per-input SHA-256 is re-checked under the lock (LLV7010), temp files dropped on refusal; a publish failure restores every file; the manifest struct matches RawManifest field for field; data_is_canonical mirrors the scanner and the parser's canonical compare. R5: the four codes are registered, the one index on user data follows a matched get. R3: CL-24 row, scenario and §31 statements equal the register after trimming, conformance_cl_24 asserts exact stdout, the exact changed-file set, value equality per module, the three --checks, build-root absence and nine refusals. R4 clean. Identity: no embedded input touched; surface/semantic.rs is a reader. Every item of humuhumu33's review is in the code.

Landing order: after the #91 heap half (#255 now, then #259, #262, #264, #265, #293) and the bootstrap trio; this PR needs no regeneration, so it goes in the first identity-neutral slot after those.

---

Generated by Claude Code

[afflom]

Maintainer: landing. Pushed one merge commit on this branch (no rewrite): origin/release/v0.4 at d489e6988 (with #262 and #264) merged in, and the register count set to 453 at README, SPEC §31, spec_links.rs, repository.rs and the CHANGELOG entry (the textual merge was clean and would have left every site at 452 while the register has 453 rows; validate-model and validate-spec-links say 453). The fixture lock of migrate-module-without-notation is current (lexlean lock --check clean). The PR is identity-neutral; it merges on a green gate.

---

Generated by Claude Code