feat(packages): source packages, a project imports the modules of a locked package (PK-01..PK-04)

[afflom]

Refs #161

Ready for review. Contains main at 8a84467 (with #82 and #160) and the language-1.2 records regenerated once on that combined tree. The design is the maintainer's, on #161.

What is here

• [[source_package]] (language 1.2 only; package, version, kind = "path", path), canonical-serialized after artifact_source, omitted when empty. Any other kind is LLC0101, not stubbed.
• lexlean-workspace.toml (spec, sorted members): the nearest ancestor of the project root; the project and each package path must be listed members, resolved from the workspace root; no .., no symlink, reads confined to the manifest and source_roots (SPEC §10.5).
• Lock: [[source_package]] rows (id, version, kind, source, module_prefix, tree_sha256, manifest_sha256, imports), the transitive closure. Every command recomputes them (source_package::load_locked) and refuses a mismatch with the package and both digests.
• Closed imports at link: a package module is a module of the importing project under its own prefix (PkgLib.Util); scopes import only their own modules and the packages they declare. A package definition is an ordinary definition (no module of a package is analysed for production roots, no re-export). fmt never rewrites a package file.
• Verification: package modules are generated, elaborated, replayed and audited in the importer's verify under the package's prefix; origin in the build manifest, the snapshot and the attestation (origins). source_id hashes the lock, so it carries the pins.
• Codes (R5, registered in model/errors.toml): LLC0105 pin mismatch, LLC0106 undeclared / two sources, LLC0107 prefix claimed twice, LLC0108 workspace rule, LLR3009 import of an undeclared package; symlink and escape are LLS8001.
• Register (R3): PK-01..PK-04, SPEC §31, features/suites/packages.feature, conformance_pk_01..04, fixtures under tests/packages/workspace. The register is 402 (398 on main + 4).
• SPEC §10.1/§10.5/§11/§25.1/§26.3, CHANGELOG, README, and the plants in VERIFICATION.md ("source packages can fail").

Decisions accepted on #161

• version is a required field of [[source_package]].
• A package manifest may declare only builtin lexicon_sources and no artifact_source or [pdf]; its glossaries are the importing project's.
• A package module's key in the importing project is its Lean name; the semantic data of a package module is read with its sibling references renamed to that key.

Records

The language-1.2 locks, oracles, fixtures, calculus files, production-export packages and verification records are regenerated once, on main 8a84467, with the repository's writers (lexlean lock, check-golden --write, check-fixtures --write, check-calculus --write, check-production-export --write, verify-examples --write). Languages 1.0 and 1.1 are byte-identical. bootstrap/ is relocked and regenerated with the rest.

Not here, on purpose

• PK-05 (the bootstrap/ pilot imports stdlib/, the vendored copy and its equivalence assertion deleted) follows as a second PR from main after this lands.

Local evidence

Linux x86-64, Lean 4.32.1, one process each: conformance_pk_01..04, vr_13, vr_23, rp_07, rp_11, rp_14, rt_01, rt_02, rt_04, sp_05, sp_09, sp_14, sl_01, lm_01..03, lm_13, bs_01; validate-model (402 ids, 85 codes), validate-spec-links, check-test-inventory, check-golden, cargo fmt --check, clippy -D warnings, cargo test -p lexlean. verify-examples was not run to the end for uor-atlas locally (language 1.0, no record moves; its Lean run was rejected on this 4-core machine); CI's Atlas leg is its evidence.

🤖 Generated with Claude Code

https://claude.ai/code/session_01AinddrUH9xHeNmR6FTWypN

[afflom]

Maintainer review: approved at f7383108.

CI. Run 39017295556 on this head: all 24 jobs green (host legs, examples, the rest leg with PK-01..PK-04, the four bdd-* rows, the 14 Atlas jobs and atlas (join)), plus repro and honesty. The head contains main 8a844674 (#160), still main's tip, and is clean.

Against #161, point by point (SPEC §10.5, the code, the register).

• A package is a project, imported by pin. [[source_package]] (package, version, kind = "path", path), language 1.2 only, omitted when empty so a project without one keeps its bytes; any other kind is LLC0101, refused, not stubbed.
• The workspace rule is stated narrowly: lexlean-workspace.toml lists member directories; a project that declares a package must be a member and a path must name a member; a stray file higher up grants nothing to a project it does not list; .. and symlinks are LLS8001; only a package's manifest and the files under its source_roots are read (LLC0108 for the workspace violations).
• Locked. The lock carries [[source_package]] rows (id, version, kind, source, module prefix, tree_sha256, manifest_sha256, imports) over the transitive closure; every command recomputes them and a changed byte, version, source, prefix or declaration is LLC0105 naming the package and both values; an unreached row or one id with two sources is LLC0106.
• Closed. A scope imports only its own modules and the packages it declares (LLR3009 for one the closure holds but the scope does not declare; LLR3005 for one nobody provides; LLC0107 for a prefix claimed twice or a name both provide; LLR3003 for cycles).
• Production and verification, as designed. A package definition is an ordinary definition (no re-export; no package module is analysed for roots); package modules are generated, elaborated, replayed and audited in the importer's verify under the package's prefix, with their origin in the build manifest, snapshot and attestation; source_id hashes the lock.
• R3, R5. The register rows PK-01..PK-04, SPEC §31, the scenarios and the failing tests come first in the history; the five new codes are registered in model/errors.toml and audit-errors passes; plants and their red output are in VERIFICATION.md ("source packages can fail"); languages 1.0 and 1.1 records are unchanged (check-golden).
• Identity. The schema change moves the language-1.2 compiler-semantics ID once; the records of every 1.2 project were regenerated on the combined tree (2,225 files), which is why this PR touches them.

Two decisions I accept, both in the PR and to be lifted by a later issue, not silently: version is a required field of [[source_package]], and a package manifest declares builtin lexicon sources only and no artifact_source or [pdf].

Not in this PR, on purpose. PK-05 (the bootstrap/ pilot imports stdlib/, the vendored copy and its equivalence assertion are deleted) is the session's next, small PR from main; #161 stays open until it lands.

Merging with a merge commit pinned to this head. Every other PR with language-1.2 records now merges main and regenerates once.

---

Generated by Claude Code