feat(packages): the bootstrap pilot imports the stdlib; the vendored Text is deleted (PK-05, #161)

CHANGELOG.md

@@ -34,8 +34,10 @@ versions, and the entries below say what each tag does and does not claim.
   never writes a package file. The schema change moves the language-1.2
   compiler-semantics ID once; languages 1.0 and 1.1, and a language-1.2 project
   without source packages, keep their bytes apart from that identity. The
-  register gains `PK-01`..`PK-04` (401 rows with `SL-01` and `LM-01`..`LM-03`, `LM-13`); `PK-05` (the `bootstrap/` pilot
-  imports `stdlib/`) follows #153 and #160.
+  register gains `PK-01`..`PK-05` (403 rows with `SL-01`, `BS-01`, and `LM-01`..`LM-03`, `LM-13`); `PK-05`: the `bootstrap/`
+  pilot imports `stdlib/` through a source package, its vendored copy of `Text`
+  and the equivalence assertion of `BS-01` are deleted, the repository gains a
+  root `lexlean-workspace.toml`, and `xtask` stages a project with its packages.
 - The first component of the compiler's own pipeline as language-1.2 source:
   the exact axiom-output parser (SPEC.md §17.23, §22.5, `BS-01`, #92 step 4;
   no new diagnostic code, no change to the language-1.2 identity).

CONFORMANCE.md

@@ -344,6 +344,7 @@ the error registry does not sanction (R5, `ERRORS.md`).
 | `PK-02` | `build` | A module of a project imports only modules of its own project and modules of the packages the project declares, and a module of a package only modules of itself and of the packages its own manifest declares: a package module is a module of the importing project under its own module prefix, a module of a package the project does not declare fails with LLR3009, and an import cycle through a package fails with LLR3003. |
 | `PK-03` | `build` | An importing project builds and verifies under the pinned Lean offline, and its package modules are generated, elaborated, replayed with `leanchecker`, and audited for their exact axioms under the package's module prefix with the package as their origin in the records; the source ID of the project changes with the pins, and no file of the package is written by `fmt`, `build`, or `verify`. |
 | `PK-04` | `build` | A production root of the importing project whose closure reaches a definition of a package certifies and exports over that closure as it does for a definition of its own module, the `production:` roots of a package are not roots of the importing project, and the importer publishes no certificate of the package's own. |
+| `PK-05` | `build` | The `bootstrap/` pilot imports the standard library's `Text` module through a source package of the workspace instead of holding a copy: its configuration declares `stdlib` as a source package, `bootstrap/src/` holds no `Text` module, `check` links `LexLeanStd.Text` as a module of the project whose definitions are ordinary ones, so that the project's production roots remain `parseAuditOutput` and `isClosedLeanName`, and neither the case of `BS-01`, SPEC.md §17.23, nor `bootstrap/README.md` keeps the copy or its equivalence assertion. |
 
 ## preservation
 

README.md

@@ -142,7 +142,7 @@ just vv        # the complete normative acceptance gate (SPEC.md §9.2)
 just release   # vv, then the §30 release criterion; refused until 1.0.0
 ```
 
-All 402 registered conformance IDs are implemented and pass; `just vv` runs clean from a checkout with the pinned toolchain installed.
+All 403 registered conformance IDs are implemented and pass; `just vv` runs clean from a checkout with the pinned toolchain installed.
 
 The differential against the independent generator `lean4-prod` (SPEC.md §17.19, `OR-01`..`OR-08`) acquires it at its pinned commit: from the checkout `LEXLEAN_ORACLE_DIR` names, or by fetching the commit with `git` into the Cargo target directory (`LEXLEAN_ORACLE_CACHE` overrides), and builds it with the pinned Lean and Rust toolchains. It is validation evidence only and no input to any identity. An oracle that cannot be acquired, is not the pinned files, or fails is unavailable: that fails the gate on Linux x86-64 and is printed as `NOT VALIDATED` elsewhere, and is never reported as agreement.
 
@@ -184,7 +184,7 @@ Every row is validated by `just vv`; the IDs link the claim to its register row,
 | The runtime of generated Lean as native modules: the portable, collection, model, and reasoning runtimes of language 1.2 are LexLean source that every generated module imports, migrated losslessly and audited against their exact axioms, the released runtime text of languages 1.0 and 1.1 is frozen data equal to their released output, and no other Lean runtime text remains in the compiler but the decoder of core module 2 | `RT-01`..`RT-04` | `build` |
 | The standard library: language-1.2 source beside the compiler whose members are certified production roots, each validated against Rust's standard library by a seeded differential of its evaluator and rustc realizations; bytes and text over `Bytes` | `SL-01` | `build` |
 | The bootstrap project: the compiler's own components as language-1.2 source compiled by LexLean's production pipeline to certified Rust packages, the first being the exact axiom-output parser and its closed Lean-name check, each held to the Rust it replaces (the stage-0 oracle) by the committed golden vectors and a seeded differential of its evaluator and rustc realizations, with planted defects detected and the production export committed | `BS-01` | `build` |
-| Source packages: a language-1.2 project imports the modules of a locked, content-addressed package of its workspace: `[[source_package]]` and `lexlean-workspace.toml`, the pins in `lexlean.lock` recomputed by every command, imports closed at link, no re-export of a package's production roots, and the package's modules replayed by the importer's `verify` with their origin in the records | `PK-01`..`PK-04` | `build` |
+| Source packages: a language-1.2 project imports the modules of a locked, content-addressed package of its workspace: `[[source_package]]` and `lexlean-workspace.toml`, the pins in `lexlean.lock` recomputed by every command, imports closed at link, no re-export of a package's production roots, and the package's modules replayed by the importer's `verify` with their origin in the records | `PK-01`..`PK-05` | `build` |
 | The literal `nat-add-zero` example, the Lean-verified feature examples, and the complete negative fixture suite | `EX-01`..`EX-08` | `build` |
 | Language-1.2 text components, first slice: tokenizers and their round-trip laws, with the laws carried as one native core module the generated modules import rather than authored Lean text (context windows, text generators, text classifiers, adapters, and composition follow in their own slices and add their rows then) | `LM-01`, `LM-02`, `LM-03`, `LM-13` | `build` |
 

SPEC.md

@@ -868,6 +868,8 @@ members = ["app", "base", "lib"]
 
 **The pin.** `lexlean.lock` (§11) carries one `[[source_package]]` row for every package in the transitive closure of the project's declarations, sorted by `id`: the identifier, the declared `version`, `kind`, the workspace-relative `source`, the package's `module_prefix`, `tree_sha256` over the package's `lexlean.toml` and every regular file beneath its `source_roots` (the tree digest of §11.5, over package-relative paths in bytewise order), `manifest_sha256` over its `lexlean.toml`, and `imports`, the `id@version` of the packages its own manifest declares, sorted. The digests are recomputed by every command: `lock --check`, `check`, `fmt`, `build`, and `verify` read the package and require the lock's row to be the package as it now is. A changed byte, a changed version, source, prefix, or declared package is `LLC0105`, naming the package and the locked and the found values, before anything is linked. A row for a package the closure of the project's declarations does not reach is `LLC0106`, and so is one identifier with two sources. `lexlean lock` writes the rows, and a package that depends on itself or on the importing project is `LLR3003`.
 
+Two limits of this release are deliberate. `version` is required in a `[[source_package]]` table because a changed version must be refused and the pin is the digest, so there is nowhere else to write it; and a package manifest declares only builtin `lexicon_source`s and no `artifact_source` or `[pdf]`, because those would name files outside the manifest and source roots that the pin covers. A later release lifts the first by a lock that records a version the package itself declares, and the second by pinning the files such a declaration names in the package's tree digest and resolving them from the package's own root; each is a separate register row, not a hidden default.
+
 **One source per module prefix.** The importing project's prefix and each package's must not be equal, and none may lie beneath another (`a.b` is beneath `a`); two sources that claim a prefix are `LLC0107`.
 
 **Closed imports.** A module of the importing project may import modules of the project, written as before, and modules of the packages the project declares itself, written with the package's prefix: `\importmodule{LexLeanStd.Text}`. A module of a package may import the modules of that package, written as inside the package, and the modules of the packages its own manifest declares, written with their prefixes. A module of a package the importing scope does not declare, though the closure holds it, is `LLR3009`; one no source provides is `LLR3005`; a name both the scope's own modules and a declared package provide is `LLC0107`; a cycle of packages or of modules is `LLR3003`. The package's modules that no import reaches are not linked. Inside the linked project a package module is named by its Lean name, `LexLeanStd.Text`, which is its key in every record; its references to a sibling are read under that key.
@@ -6682,15 +6684,13 @@ library does. The Rust it replaces stays in the tree as the *stage-0 oracle*
 until the fixed point of that plan; a component is added only with a
 differential against that Rust, and is never a source of the Rust.
 
-A project reads only its own source roots (§10.1: a source root is a
-project-relative path that names no parent directory, and a symbolic link is
-refused), so a project cannot import another's modules. The module `Text` of
-the standard library (§17.22) is therefore present in `bootstrap/src/` as a
-copy of `stdlib/src/Text.lex.tex` in which the `production` declarations are
-removed, so that the copy is a library of the project and republishes none of
-the standard library's packages. `BS-01` compares the copy with the standard
-library's module on every run, and it is removed when a project can depend on
-another.
+The project imports the module `Text` of the standard library (§17.22) as a
+source package (§10.5): `bootstrap/lexlean.toml` declares `stdlib` beside it in
+the workspace, `AxiomOutput` imports `LexLeanStd.Text`, and the module is
+linked, verified, and replayed with the project under the standard library's
+own prefix. Its definitions are ordinary definitions of the project, so the
+project republishes none of the standard library's production roots, and no
+copy of the module is kept (`PK-05`).
 
 The first component is the axiom-output parser (§22.5), the module
 `AxiomOutput`, with two production roots for `rust-std`:
@@ -9548,12 +9548,13 @@ Every row below is normative, has honesty level `build`, and MUST be copied byte
 | `PK-02` | `packages` | A module of a project imports only modules of its own project and modules of the packages the project declares, and a module of a package only modules of itself and of the packages its own manifest declares: a package module is a module of the importing project under its own module prefix, a module of a package the project does not declare fails with LLR3009, and an import cycle through a package fails with LLR3003. | §10.5, §15.1 |
 | `PK-03` | `packages` | An importing project builds and verifies under the pinned Lean offline, and its package modules are generated, elaborated, replayed with `leanchecker`, and audited for their exact axioms under the package's module prefix with the package as their origin in the records; the source ID of the project changes with the pins, and no file of the package is written by `fmt`, `build`, or `verify`. | §10.5, §21.3, §22 |
 | `PK-04` | `packages` | A production root of the importing project whose closure reaches a definition of a package certifies and exports over that closure as it does for a definition of its own module, the `production:` roots of a package are not roots of the importing project, and the importer publishes no certificate of the package's own. | §10.5, §17.13 |
+| `PK-05` | `packages` | The `bootstrap/` pilot imports the standard library's `Text` module through a source package of the workspace instead of holding a copy: its configuration declares `stdlib` as a source package, `bootstrap/src/` holds no `Text` module, `check` links `LexLeanStd.Text` as a module of the project whose definitions are ordinary ones, so that the project's production roots remain `parseAuditOutput` and `isClosedLeanName`, and neither the case of `BS-01`, SPEC.md §17.23, nor `bootstrap/README.md` keeps the copy or its equivalence assertion. | §10.5, §17.23 |
 | `LM-01` | `language-models` | A `tokenizer` is a closed language-1.2 declaration whose scheme is `byte_level` or `longest_match` and whose vocabulary is a #29 artifact with role `vocabulary` and schema `utf8_lines`; tokens are `uint32`, the single bytes are the ids 0..255 present always as the byte fallback, the vocabulary pieces take the ids from 256 in artifact order, and the declaration elaborates to `encode` and `decode` over `bytes` together with `encodeText` and `decodeText` over `string` through `utf8_encode` and `utf8_decode`, so a scheme outside the closed enumeration, a vocabulary whose role or schema is not the one stated, or a token outside `uint32` is refused as a schema violation (`LLT4001`) or by the artifact rules (`LLR3007`). | §17.12 |
 | `LM-02` | `language-models` | A tokenizer's laws are generated and kernel-checked: `roundtrip` states that for every byte string `b`, `decode (encode b)` is `some b`; `text_roundtrip` states the same over `string`; and `in_range` states that every token a decode produces indexes the vocabulary, so the round trip also fixes the token boundaries, and a tokenizer whose elaboration does not close these laws fails verification. | §17.12 |
 | `LM-03` | `language-models` | Text that is not valid UTF-8 is refused and never tokenized: an artifact whose bytes do not decode under the `utf8_lines` schema — invalid UTF-8, a CR, or a missing final LF — fails by its artifact rules before any byte is decoded, and a text offered to `encodeText` that is not valid UTF-8 is refused rather than transcoded. | §17.12 |
 | `LM-13` | `language-models` | The text laws a tokenizer elaborates through are LexLean source and not authored text: the module that states them is one language-1.2 native core module of the embedded `language/text-1.2` project, the project holds no file of Lean source, no independently authored Lean file anywhere in the release tree declares the `LexLeanText` namespace or lies under its module root, and the one-time migration input is absent; the registry lists only that module, the declarations and their exact axiom policies are read from its native data, which the compiler embeds and hashes into the language-1.2 semantics, and a module that declares a text component imports the generated module rather than splicing any Lean text. | §17.10, §17.12 |
 
-**Total required capability IDs:** 402.
+**Total required capability IDs:** 403.
 
 No row may be downgraded to `some-true` or `open`. Upstream Lean facts are ledger/authority rows, not substitutions for these build behaviors.
 

bootstrap/README.md

@@ -2,11 +2,11 @@
 
 The compiler's own components as language-1.2 source (SPEC.md §17.23, issue 92).
 
-`src/Text.lex.tex` is **temporary**. It is a copy of `stdlib/src/Text.lex.tex`
-with the `production` declarations removed, kept here only because a project
-reads its own source roots and cannot import another project's modules
-(`config::is_project_relative` refuses `..`, and symbolic links are refused).
-The `.lex.tex` notation has no comment form (§17.21.5), so this note is the
-header the copy cannot carry. `BS-01` asserts on every run that the copy is the
-standard library's module without its `production` declarations; delete the
-copy, and that assertion, when a project can depend on another.
+`src/AxiomOutput.lex.tex` imports the standard library's `Text`
+(`stdlib/src/Text.lex.tex`) as a source package: `lexlean.toml` declares
+`stdlib` beside this project in the workspace (`lexlean-workspace.toml`), the
+lock pins it by digest, and its modules are linked, verified, and replayed with
+this project under their own prefix `LexLeanStd` (SPEC.md §10.5). Its
+definitions are ordinary definitions here, so this project republishes none of
+the standard library's production roots. The `.lex.tex` notation has no comment
+form (§17.21.5), so this note is the header the sources cannot carry.