[v0.4] Source packages: a project imports the modules of a locked, content-addressed package (needed by #92's stdlib and #32)

@humuhumu33

Child of #92 and #32; found by the pilot of #160.

Why this is on the v0.4 path

Two v0.4 issues need something LexLean does not have:

[v0.4] Build model/reasoning stdlib composition and PrismPM application fixture #32 (DoD): "Packages are locked, closed, independently reusable"; acceptance: "Replacing a package version/digest or introducing an unregistered semantic dependency fails".
[v0.4] #27 stage 8: the production compiler authored in .lex.tex and compiled by LexLean to production software #92 (order, step 2): "a package of modules the compiler project imports". The first pilot (feat(bootstrap): the axiom-output parser as language-1.2 source (BS-01) #160) had to vendor stdlib/src/Text.lex.tex into bootstrap/ and assert the copy equals the original on every run, because a project cannot import another project's modules: it reads only its own source_roots (config::is_project_relative rejects ..; symlinks are refused). The [[lexicon_source]] kinds (builtin, path, git) carry glossary phrases only.

Without a mechanism, the stdlib (#153 and its successors, #126), the compiler project and the model/reasoning libraries of #32 can only be used by copying, which is not "locked" and not "closed".

Proposal (language 1.2 only; languages 1.0 and 1.1 stay byte-identical)

A package is a project. Its own lexlean.toml (name, module_prefix, source_roots, language 1.2, and its own package dependencies); entrypoints may be empty for a library. Its modules keep its own module prefix, so LexLeanStd.Text is LexLeanStd.Text in every project that imports it.
Declared in the importing project. [[source_package]] tables (sorted by package; omitted entirely when there are none, as artifact_source is, so existing projects keep their bytes): package (an identifier), kind = "path", path. Only path in this issue: nothing is fetched at build (§25), which is what "offline after setup" in [v0.4] Build model/reasoning stdlib composition and PrismPM application fixture #32 needs. A git kind for source packages is out of scope and refused, not stubbed.
Where a path may point. Today's rule keeps every read inside the project. A package lives beside the projects (stdlib/ beside compiler/), so the rule needs one widening, stated narrowly: an optional lexlean-workspace.toml at the repository root lists the member project directories; a source_package path must name a member, resolved from the workspace root; no .. beyond it, no symlinks, reads confined to the member's source_roots and manifest (§25.1). A project outside any workspace cannot declare a source package (the diagnostic says so).
Locked. lexlean.lock gains [[source_package]] entries like the lexicon [[package]] ones: the package id, tree_sha256 over the package's manifest and source files in canonical order, manifest_sha256, and its imports (its own package dependencies, transitively). lexlean lock computes them; lock --check and every other command recompute and refuse a mismatch with a registered code (LLC01xx), naming the package and both digests. Replacing a package's version or any byte is therefore a refusal, as [v0.4] Build model/reasoning stdlib composition and PrismPM application fixture #32 requires.
Closed. A module may import only modules of its own project, or of a package the project declares; a package module only modules of itself or of packages its own manifest declares. Linking refuses anything else (an "unregistered semantic dependency"), and a module prefix claimed by two sources is refused.
Production. A package's production: clauses make roots of the package project, built when the package is built. Imported by another project, a package definition is an ordinary definition: certificates are made over the closure of the importing project's roots, and the package's own certified packages are not republished by the importer. (No re-export in this issue; if wanted it is a later, separate row, not a hidden default.)
Verification. The package's modules are generated, elaborated, replayed and audited as part of the importing project's verify, under the package's prefix, with their origin in the records. Nothing crosses runs (§9.4); there is no cache of a built package.
Identity. The importing project's source_id includes the pins. The schema change (source_package, the lock section) moves the language-1.2 compiler-semantics ID once. Landing order: with or right after feat(core): derived rows are made by Lean's reserved-name actions and checked (SM-33, stage 2 of #91, part 1) #155 and feat(language-1.2): tokenizers over the native text laws (LM-01..LM-03, LM-13; part of #30) #82, in the same regeneration wave (feat(core): derived rows are made by Lean's reserved-name actions and checked (SM-33, stage 2 of #91, part 1) #155 changes the decoder; feat(language-1.2): tokenizers over the native text laws (LM-01..LM-03, LM-13; part of #30) #82 moves the identity on its own), so the language-1.2 records are regenerated once, not three times.

Register, R3

A suite packages, rows such as PK-01 (config and lock round trip; refusals: digest changed, undeclared package, prefix collision, path escaping the workspace, a symlink, a package outside a workspace), PK-02 (import closure at link), PK-03 (an importing project verifies under the pinned Lean with exact axioms, package modules replayed), PK-04 (a production root whose closure reaches a package definition certifies), PK-05 (the bootstrap/ pilot imports stdlib/ and the vendored copy and its equivalence case are deleted). The statements are written with the rows; plants in VERIFICATION.md.

Acceptance

Fresh build and verify of an importing project succeeds offline.
A changed byte, a changed version, an undeclared package, a duplicate prefix and an escaping path each fail with a named code.
The bootstrap/ pilot (feat(bootstrap): the axiom-output parser as language-1.2 source (BS-01) #160) and the stdlib (feat(stdlib): the first member, bytes and text over Bytes (#92) #153) use it; no vendored copy remains.
Languages 1.0/1.1 byte-identical; 1.2 identity regenerated once and recorded; full just vv.

Not in scope

Registries, semver resolution (the pin is the digest; a version string is for readers), fetching, and publishing a package as a crate. The models' and reasoning's own libraries (#32) are packages of this kind and come after it.

Process

Written by the maintainer to fix the design before anyone builds it. @humuhumu33: objections or amendments in the next hour (especially 3, the workspace rule, and 6, no re-export) are welcome; if there are none a contributor session starts on it, stacked on main, with the identity change coordinated with your #155 and #82.

@humuhumu33

No objection in the hour, so a contributor session has started on this: branch claude/issue-161-source-packages from main, draft PR to follow (Refs #161). The design above is its specification; it will post its lock format and its workspace rule here before it builds them, so objections are cheapest there. @humuhumu33: amendments to 3 (the workspace rule) or 6 (no re-export) go on this issue, and the session follows them.

The identity move is the one coordination point: the schema change moves the language-1.2 compiler-semantics ID once, and #155 (decoder) and #82 (tokenizers, which moves the identity on its own) land first. The session develops with locally regenerated records and does not regenerate the committed ones until I say so, so nobody regenerates twice for this.

Generated by Claude Code

@humuhumu33

Contributor session, plan before building (objections cheapest here, @humuhumu33 @afflom). Language 1.2 only; a project without source_package keeps its bytes.

Config (importing project)

[[source_package]]
package = "std"          # identifier, sorted, unique
version = "1.0.0"        # for readers; pinned in the lock
kind = "path"            # any other kind: LLC0101, not stubbed
path = "stdlib"          # a workspace member, resolved from the workspace root

version is the one field beyond the issue's list: #161 says a changed version must be refused, and a version needs somewhere to be written. It is required, a reader's string, and changing it is the same refusal as changing a byte.

Workspace rule — lexlean-workspace.toml at the repository root:

spec = "lexlean/workspace/1"
members = ["compiler", "stdlib"]   # sorted, unique, workspace-relative project directories

The workspace is the nearest ancestor of the (canonicalized) project root holding that file. The importing project must itself be a listed member, and a source_package path must be a listed member, so a stray file up the tree grants nothing. No .., no absolute path, no symlink component from the workspace root down; the package is read only through its manifest and its source_roots. Outside a workspace, or not a member: LLC0108.

Package manifest — its own lexlean.toml, language 1.2, with its own [[source_package]]. It may declare only builtin lexicon_sources and no artifact_source or [pdf] (those would read outside the confined set); its \useglossary must resolve in the importing project's closure. entrypoints may name any module (a library lists one).

Lock — lexlean.lock (lock/2) gains, sorted by id, the transitive closure:

[[source_package]]
id = "std"
version = "1.0.0"
kind = "path"
source = "stdlib"
module_prefix = "LexLeanStd"
tree_sha256 = "…"     # `tree_digest` over lexlean.toml + every regular file under its source_roots, member-relative, byte order
manifest_sha256 = "…"
imports = ["other@1.0.0"]   # its own declared packages

Every command recomputes the tree and refuses a mismatch with the package and both digests (LLC0105). A package id used with two sources, or one prefix claimed by two sources (or the project's own), is LLC0106; an import of a module that is neither the project's nor a declared package's is LLR3009; a symlink or escaping path is LLS8001.

Linking — a package module's key in the importing project is its full Lean name (LexLeanStd.Text), imported as \importmodule{LexLeanStd.Text}; inside the package it keeps its own relative imports. Its definitions are ordinary definitions: its production: roots are not roots of the importer (no re-export), fmt never rewrites a package file, and verify generates, elaborates, replays and audits the package modules under its prefix, with the package id as origin in the records. source_id already hashes the lock, so it carries the pins.

New codes: LLC0105..LLC0108, LLR3009. PK-05 waits for #153/#160 on main; I will say so on the PR rather than register a row I cannot run.

Generated by Claude Code

Draft PR: #162 (Refs #161). Implemented as posted above; main merged once (#153, #159).

Ready to regenerate the language-1.2 records, on the maintainer's word: PK-01..PK-04 pass locally, and the identity move (project/lock/manifest/attestation/snapshot v2 schemas) is final unless review changes it. I have not regenerated or committed any language-1.2 lock, oracle, fixture or record; the gates that compare them are red on #162 by identity alone until that wave. In a scratch worktree (not pushed) I regenerated locks and ran check-golden --write and verify-examples --write: every language 1.0/1.1 oracle is byte-identical, and a language-1.2 example without a source package changes in identities and the digests derived from them only.

PK-05 waits for #160: stdlib/ is on main, bootstrap/ is not. I will add it as a later commit on #162 once #160 lands, and will not register a row I cannot run.

Two choices to confirm, both in the PR description: version is a required field of [[source_package]], and a package manifest may declare only builtin lexicon_sources and no artifact_source/[pdf].

Generated by Claude Code

For the PK-05 step: #160 vendors stdlib/src/Text.lex.tex into bootstrap/src/Text.lex.tex (without its production: clauses) because a project cannot import another's modules today. It is temporary until source packages land. When PK-05 lands, delete the copy, the equivalence assertion in BS-01 (vendored_text() in crates/conformance/src/cases/bootstrap.rs, and the first assertion of the case), bootstrap/README.md, and the paragraph about the copy in SPEC §17.23 (the sentence that names this issue and PK-05, committed locally on the #160 branch and carried into its next push). bootstrap/ then imports LexLeanStd.Text and regenerates (identity unchanged by the removal, but the project's records and exported packages change with the module set).

Generated by Claude Code

chore(#161): regenerate the language-1.2 records on the combined tree…

chore(#161): regenerate bootstrap/ and the records of compiler, stdli…

#162 is pushed once (head f738310) and marked ready. It contains main at 8a84467 (#82, #160 and the rest), the language-1.2 records regenerated once on that combined tree, and the register at 402 (398 + PK-01..PK-04).

Regenerated with the repository's writers, on the merged tree: lexlean lock of every committed language-1.2 lock (the one deliberately mismatched fixture lock, lock-schema-language-mismatch, keeps its lexlean/lock/1 and takes only the new semantics ID), check-golden --write, check-fixtures --write, check-calculus --write, check-production-export --write, verify-examples --write. bootstrap/ is relocked and its records regenerated with the rest.

Passing locally (Linux x86-64, Lean 4.32.1), one process each: pk_01..pk_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..lm_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. rp_11 failed first (the README capability table did not claim the PK rows); fixed.

Not run to the end locally: verify-examples for uor-atlas. It is language 1.0, so none of its records move, but on this 4-core machine its Lean run was rejected (CensusCert10, no message), so the run covered the other examples, compiler, stdlib and bootstrap; CI's Atlas leg is the evidence for it. check-golden passes on all of them, uor-atlas included.

PK-05 is next, as a second commit on #162, not in this push: it imports stdlib as a source package into bootstrap/, deletes bootstrap/src/Text.lex.tex and the equivalence assertion in BS-01, fixes the 'temporary' sentences in SPEC §17.23 and bootstrap/README.md, and adds the root lexlean-workspace.toml. The SPEC note that version is required and that a package manifest declares builtin lexicon sources only and no artifact_source/[pdf] are deliberate, and what lifts them, goes in that commit too. I did not check the Windows host leg for PK-04; it exports and replays the bundle and does not build the generated Rust package with rustc.

Generated by Claude Code

Merge pull request #162 from UOR-Foundation/claude/issue-161-source-p…

PK-05 is up as #165 (Closes #161), on main ea0a4ed: the bootstrap/ pilot imports stdlib/ as the source package std (LexLeanStd.Text), bootstrap/src/Text.lex.tex and BS-01's equivalence assertion are deleted, a root lexlean-workspace.toml lists bootstrap and stdlib, and xtask stages a project with its packages. Only bootstrap/'s records are regenerated; no identity moves. The register is 403.

Ran locally (Linux x86-64, Lean 4.32.1): conformance_pk_05, pk_01, bs_01 (444 s), sl_01, rp_07, rp_11, rp_14; validate-model, validate-spec-links, check-test-inventory, check-golden, fmt, clippy. The by-item acceptance is in the PR body; the full just vv item is #165's own CI run, as it was #162's.

Generated by Claude Code

Merge pull request #165 from UOR-Foundation/claude/issue-161-pk-05

Navigation Menu

Repository navigation

[v0.4] Source packages: a project imports the modules of a locked, content-addressed package (needed by #92's stdlib and #32) #161

Why this is on the v0.4 path

Proposal (language 1.2 only; languages 1.0 and 1.1 stay byte-identical)

Register, R3

Acceptance

Not in scope

Process

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

[v0.4] Source packages: a project imports the modules of a locked, content-addressed package (needed by #92's stdlib and #32) #161

Description

Why this is on the v0.4 path

Proposal (language 1.2 only; languages 1.0 and 1.1 stay byte-identical)

Register, R3

Acceptance

Not in scope

Process

Activity

afflom commented on Oct 17, 2026

afflom commented on Oct 17, 2026

afflom commented on Oct 17, 2026

afflom commented on Oct 17, 2026

afflom commented on Oct 17, 2026

afflom commented on Oct 17, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions