Repository navigation
[v0.4] #27 stage 3: the LexLean authoring surface: a human-writable .lex.tex syntax, an SDK API, and no other authoring path #93
Description
Child of #27; decision recorded in this comment. Delivery stage 3, the critical path: #89, #91, #84 and #92 depend on it (#90 does not).
Decision (maintainers, 2026-10-14)
The repository has to include its own authoring surface, with an SDK/API or equivalent. .lex.tex is the only authorized authoring surface of LexLean. Everything the compiler, the libraries and the models are made of is authored there, by a person or through the SDK, and nothing else is a source.
The gap, measured on main (d284b165)
- Language 1.0/1.1 declarations have a human surface (
\begin{typedefinition},\begin{theorem}, the structured proof language of §16, closed glossaries of §13). Language 1.2's semantic modules do not: a source is\begin{semanticmodule}\semanticdata{{"declarations":[{"constructors":[…(canonical JSON, one line); the 15 declaration kinds (structure,class,instance,inductive,definition,theorem,artifact,contract,realization,evidence,model,logic,inference_rule,verifier,reasoner), 43 term kinds, 12 type kinds and 10 proof kinds oflexlean/semantic-module/2can only be written by writing JSON. - The compiler's own sources (
compiler/models of the target calculus and the Rust machine, GNAF, the certification model, the tooling modules, every example, the MNIST project) are produced by Rust builders incrates/conformance/src(calculus_source.rs,rust_source.rs,gnaf_model.rs,certification_model.rs,lcnf_*.rs,tl.rs,lx.rs) and checked bycargo xtask check-calculus. The builders are the real authoring surface and they live in apublish = falsetest crate: the repository ships a compiler for a language whose sources it cannot write. - Core modules (
lexlean/core-module/2, the native proof libraries: 4,396 declarations in the preservation and certification libraries, the Atlas at 24 MB) are lossless exports of kernel terms: all arguments explicit, no tactic, no notation. They can be read by the compiler and by Lean, not edited by a person. - The compiler already prints a terse typed form of every semantic term, type, proof and claim for the canonical document (
examples/language-1.2/expected/build/modules/LanguageTwelve/Main.tex:Definition: (let doubled : Nat := (n + n); (doubled + 1))), so a surface that a person can read exists in one direction.
Design (proposal; work proceeds unless objected to)
1. The surface is the canonical document syntax, made parseable
For language 1.2 the source of a semantic module is the closed form its canonical document already prints, in a fixed grammar (SPEC §15, like the structural grammar: environment and control names are literal core entries, identifiers are declared names, no free prose):
\begin{semanticmodule}
\begin{definition}{doubledSuccessor}
\parameters{(n : Nat)} \type{Nat} \noaxioms
(let doubled : Nat := (n + n); (doubled + 1))
\end{definition}
\begin{theorem}{doubled_successor_two}
\noaxioms (doubledSuccessor 2 = 5)
\begin{proof} reflexivity \end{proof}
\end{theorem}
\end{semanticmodule}
(The exact shape is for the SPEC section and the first PR to fix; the point is the grammar covers the whole closed schema, with every keyword a registered core entry, so the closed-lexicon discipline of §13 is kept.)
The laws, each a registered conformance ID with its own scenario and test (R3):
- Round trip on the data: for every committed semantic module
d,parse(print(d)) = d; the printer is total over the closed schema. fmtcanonical and idempotent:fmt(fmt(s)) = fmt(s);fmtaccepts the legacy\semanticdataform of a language-1.2 module only to rewrite it to the surface, once.- Exhaustive by construction: a new semantic variant cannot be added without a printer arm, a parser production, a schema row and a round-trip case (a structural audit in the manner of
audit-production; [v0.4] Add language-model semantic components and compositional text-processing pipeline #30's new declaration kinds, for example, must arrive with their surface). - No panic on any single-node mutation of a committed source (as
TL-01), with the closed error model (R5), source maps, and coverage.
2. The SDK
A public API of the shipped lexlean crate (§24), not of the conformance crate: the typed data model of the modules (already crate::ir; made public, serde, versioned), parse/print/fmt/elaborate over it with spans and diagnostics, and the builders the conformance crate has today (moved in, typed, validated against the registries). Anything that produces a source goes through the printer, so what it writes is canonical .lex.tex; the output is a source only in the sense that it is committed and reviewed as one.
3. No other authoring path
- Every committed source of the repository's own models becomes surface
.lex.tex, hand-written and hand-edited from then on.check-calculus --writeand the other writers that regenerate sources from Rust builders are removed; the check that remains is the parse, link and verification of the committed source, plus the Rust-side tests that now load sources rather than compare them with builder output. - The builders in
crates/conformancethat generate test inputs may stay as test tooling, but none may own a committed source of the product (compiler/,language/,examples/). - A permanent gate states this (in the manner of
VR-19): no source file under those trees is the output of a generator, i.e.fmtis the identity on all of them and no builder output is compared with them.
4. Core modules and proofs
The native libraries need two things to become editable: (a) a printer that renders kernel terms readably, losslessly (explicit arguments, universe levels, named binders), so they become source in the same grammar; and (b) a front end that elaborates a surface (implicit arguments, universe inference, notation, structured proofs lowering to terms) into core-module data, so a person can add a theorem. The front end is not in the trusted base: its output is a kernel term and Lean's kernel checks it, as for every other module (Lean verifies LexLean). This is the largest part and comes last.
Staging (each a PR with its own proofs and plants)
- 3a semantic modules: the SPEC section and registered IDs; parser and printer for the 15 declaration kinds, 43 term kinds, 12 types, 10 proofs;
fmt; the round-trip gate over every committed semantic module; the public API; migration of the compiler's own semantic sources and the examples to the surface (a regeneration PR, no semantic change). - 3b tooling modules: the same family for
lexlean/tooling-module/1; the stage-1 adapter's sources migrated. - 3c core modules: the lossless printer; the committed libraries and the Atlas migrated to the surface; round trip.
- 3d the elaborating front end for core modules (the proof-authoring surface); the library gains a theorem authored in it, kernel-checked, as the first user.
- 3e the SDK documented in SPEC §24,
lexlean inittemplates, the permanent no-other-authoring-path gate, builders for product sources removed.
DoD
- A person can write, format, check, build and verify a language-1.2 project, including a model, a contract and a proof, from
.lex.texalone, in an editor, with no JSON and no Rust. - Every committed
.lex.texsource of the repository is in the surface;fmtis the identity on all of them; the parse of each equals the data the build used before the migration (equivalence record). - The public API parses, prints and elaborates, and the repository's own tests use it.
- The no-other-authoring-path gate passes and is shown to fail on a planted generator output.
Acceptance criteria
- Round trip and
fmtidempotence over every committed module (semantic, tooling, core). - Planted defects each turn a named gate red: a printer arm dropped, a parser production dropped, a non-canonical source, a source regenerated from a builder, a new variant without surface.
- Languages 1.0 and 1.1 byte-identical; language 1.2 identities regenerated and recorded.
- Full
just vv.
Questions (recommended default in each; the work proceeds on the default)
- After the migration, should language 1.2 refuse
\semanticdataoutright (default: yes at the end of v0.4; until thenfmtrewrites it)? Languages 1.1 sources keep it. - Should the surface reuse the canonical document's term syntax as is, or is a more prose-like form wanted (
Define the function … to be …)? Default: reuse; a prose layer can be added as lexicon entries over the same grammar later without changing the data.
Activity
feat(surface): the language-1.2 authoring notation for semantic modul…
afflom commentedon Oct 14, 2026
Status of stage 3a, and what is next.
surface::{generic,semantic}, SPEC §17.21,AU-01..AU-03). It is read fromschemas/semantic-module-v2.schema.json, covers the whole closed schema (readable forms where exact, a generickind{…}form for everything else), is in bijection with the canonical JSON, and a module in it links to the semantic ID and generated bytes of its data form (checked on six examples). Both long CI legs passed; the one red leg was a macOS process-table exhaustion inend_children, a test that never reaped the children it had ended (fixed in the same push, cause in the PR thread). Re-running.fmtwrites a language-1.2 module out of its data form, and every language-1.2 source of the repository (287: thecompilerproject, examples, language libraries, fixtures, refused fixtures the notation can spell) is written in the notation;AU-04keeps it that way (the data form remains only under 1.0/1.1 and in refused fixtures the notation cannot spell). Nothing the build derives changes: same semantic IDs, same generated bytes, no verified record, no production package; only source IDs, source maps, coverage records and diagnostic positions are regenerated. I did not put asource_notationrow inlanguage/semantics-1.2.tomlafter all: it would have forced re-verifying every example for no semantic change.Next, in this order, each its own PR with plants: 3b tooling modules (
\toolingdata→ the generic notation, four committed sources), then the part of 3e the other stages wait on — the public API over the typed module data (parse/print/fmt overlexlean::ir, spans and diagnostics), and the permanent no-other-authoring-path gate with thecompiler/sources owned by the committed files instead of the builders incrates/conformance(check-calculus --writeremoved) — then 3c/3d (core modules: printer and elaborating front end). #89/#90 are with @humuhumu33 and do not depend on this; #91 depends only on semantic modules, which are now authorable.Question 1 of the issue (refuse
\semanticdataoutright under language 1.2): still the default, at the end of v0.4; until thenfmtrewrites it.Generated by Claude Code
feat(surface): tooling modules in the authoring notation, and an iden…
chore(#93): the four tooling sources are written in the authoring not…
Merge pull request #94: the language-1.2 authoring notation for seman…
afflom commentedon Oct 14, 2026
Progress, and one decision wanted.
Merged: #94 (the notation, stage 3a-A). In CI: #96 (every language-1.2 source is in the notation;
AU-04), #98 (tooling modules,AU-05; and a compiler-semantics ID that does not depend on the form a module is written in,AU-06: a source whose module is in the notation contributes its data form to the tree digest, so migrating the embedded adapter — and, at 3c, the embedded libraries — changes no identity). Next PR (built, being validated): the builders of the calculus, the Rust machine, the GNAF model and the certification model (calculus_source,rust_source,gnaf_model,certification_model, about 12,000 lines) are removed —compiler/src/{TargetSyntax,TargetSemantics,TargetOracle,RustSyntax,RustSemantics,Gnaf,Certification,Main}, the reasoning oracles and the project configuration are now written and edited as.lex.tex;lexlean::sdkis the authoring API (SPEC §24.8: read, rewrite, convert and assemble a module's source without a project; the formatter, the identity of the embedded tree and the conformance suite's own source editing are written over it); andAU-07is the permanent gate that no writer of the repository owns a product source.The decision.
AU-07as built has five exceptions, named, not pattern-matched, and pinned in the gate: the four fixture modules ofcompiler/(TargetFixtures,ReasoningFixtures,GnafFixtures,GnafCertificates) and the extraction adapter's module (language/lcnf-1.2/tooling/src/Extract.lex.tex). Each is written from an input that is not a source: the fixtures, GNAF requests and certificates are committed JSON data (a program, its arguments, and the outcome the reference interpreter computed; 1–2 MB of declarations per module that state the kernel's evaluation of each), and the adapter's module is the registry the pinned Lean itself answers (conformance_ne_04equates it with a fresh derivation). Inverting them (the Rust oracle parsing the committed module and checking the stated outcome, instead of the module being written from the Rust-defined cases) is possible but is a rewrite of the conformance crate's oracle layer (calculus.rs,gnaf.rs,certification.rs,calculus/reasoning.rs, about 9,000 lines), and what it would buy is that a fixture is added by hand-writing a large mechanical.lex.texrather than by adding a case.My recommendation: treat those five as generated oracle records — outputs of a checked comparison against an authority (a reference interpreter, the pinned Lean), as the goldens are, named by the gate, regenerated only by
check-calculus --write— and keep the gate as it is. If you want them hand-owned instead, say so and I will do the inversion as the last sub-stage of #93, before 3c/3d; nothing else in the design changes. Until I hear otherwise I proceed on the recommendation and go on to stage 3c (core modules: a lossless printer for the embedded libraries and the Atlas, then the elaborating front end).Generated by Claude Code
Merge #96: every language-1.2 source is written in the authoring nota…
Merge #98: tooling modules in the authoring notation (AU-05), a compi…
afflom commentedon Oct 15, 2026
Progress: 3a, 3b merged; 3e and 3c in CI; and what 3d is.
AU-04), feat(#93): tooling modules in the authoring notation (AU-05), and a compiler-semantics ID that does not depend on the form (AU-06) #98 (tooling modulesAU-05; an identity that does not depend on the formAU-06).lexlean::sdk(SPEC §24.8), the permanent no-other-authoring-path gateAU-07(five named generated records, nothing else), the calculus, the Rust machine, GNAF and the certification model owned by their committed.lex.tex; CI running, retargeted tomain.AU-09..AU-11): a readable program over the shared table of kernel terms whose numbering is the order of its text (every node used once is written inside its user, every other node is a labelled statement), reading back to the module, and its canonical JSON is byte for byte the committed data.compiler/proofsandlanguage/preservation-1.2/library(26 modules, 48 MB of data) are written in it at about three quarters of the size; the compiler-semantics ID of language 1.2 is unchanged (464235ad…); the Atlas stays\coredataunder language 1.0 (the compatibility lineAU-04already draws). Stacked on feat(#93): the calculus and the Rust machine are sources; the authoring API; no writer owns a product source (AU-07, AU-08) #103.3d, as I propose to build it. The issue asks for a front end that infers implicit arguments and universes and lowers structured proofs. For core modules I am not going to build inference, and I want that on the record rather than silently narrowed: a core module is a library of kernel terms whose contract is that every argument and level is explicit (that is why it is checkable by Lean's kernel with no elaborator in the trusted base, and why the Atlas and the libraries are migrated losslessly). Inference and structured proofs are what a semantic module already is under language 1.2 (the proof language of §16/§17.12, elaborated to Lean and kernel-checked by
verify; the examplespeano-arithmetic,list-induction,propositional-logicand the reasoning machines are written that way). What a person writing a kernel term lacks is not inference but names: de Bruijn indices and numeric node labels. So 3d is:const "x"), else#i; the reader resolves a name in scope to the index. Lossless by construction (the case checks it on every committed module and on a module with shadowing, outer references, clashes with constants, keyword and anonymous binders).@refl_type := …and referred to as@refl_type;fmtwrites the number. A person adds a theorem to a library by appending a declaration and two or three statements, with no counting.Eq, withEq.recand every argument explicit), kernel-checked when the library is compiled.fmtof an authored module is the canonical notation (names kept, numbers written), so an authored source and a migrated one are the same kind of file. A new register row (AU-12) states that a module written with names and symbolic labels reads to the module its canonical notation reads to. If you want a real elaborator for kernel terms instead (unification, universe inference), say so; it would be its own issue with its own trust argument and I would not fold it into #93. Until I hear otherwise I proceed on the above after #103/#104 are green.Generated by Claude Code
feat(#93): names for the variables and statements of a core module (A…
Merge pull request #103: the calculus and the Rust machine are source…
fix(#93): the library identity of a preservation record is over the d…
afflom commentedon Oct 15, 2026
#111 (L1.3 of the completion plan #106: SPEC.md and
model/*.tomlas projections of LexLean source) depends on this stage.Generated by Claude Code
Merge pull request #104: core modules in the authoring notation, with…
afflom commentedon Oct 15, 2026
#93, verified against its DoD and acceptance criteria (after #94, #96, #98, #103 and #104).
Every stage is merged: 3a #94 + #96 (semantic modules), 3b #98 (tooling modules), 3e #103 (the authoring API and the no-other-path gate), 3c + 3d #104 (core modules, names). Each line below names what discharges it; CI of each PR ran the full
just vv.DoD
.lex.texalone, with no JSON and no RustAU-01..AU-03): all 15 declaration kinds, 43 term kinds, 12 types and 10 proofs have a readable form or the generickind{…}form;examples/models(a model, a contract, evidence) andexamples/peano-arithmetic(proofs) are written in it;lexlean fmt,check,build,verifyrun over them. Tooling modules (AU-05) and core modules, with names for binders and labelled statements (§17.21.8,AU-09..AU-12), are written the same way;LexLeanCertification.authored_eq_symmis a theorem a person added to the native certification library in the notation, kernel-checked with the library by the pinned Lean.lex.texsource of the repository is in the surface;fmtis the identity on all of them; the parse of each equals the data the build used beforeAU-04(no data form in a language-1.2 product tree),AU-05,AU-09(the notation reads back to every committed core module, canonical JSON byte for byte),AU-06(the compiler-semantics ID is the data-form digest, so migrating embedded sources changed no identity: language 1.2 is still464235ad…); the equivalence records are the unchanged locks, goldens, production export and verified recordslexlean::sdk(§24.8,AU-08): read, write, convert, assemble over the typed module data, positional errors, no panics; the conformance helpers (lx.rs,tl.rs,support.rs) delegate to itAU-07: no writer of the repository emits a product.lex.texexcept five named records; plant inVERIFICATION.mdAcceptance criteria
fmtidempotence over every committed module:AU-01..AU-03(semantic),AU-05(tooling),AU-09/AU-10(core, including the 66 Atlas modules read back to their data byte for byte).VERIFICATION.md.just vv: green on each PR.What is not as the issue wrote it, with my decision on each (tell me if you want any reversed)
\coredata. It is language 1.0, core schema 1; the notation is schema 2 and refused under 1.0/1.1 (LLP2003) so that those languages stay byte-identical, which is also an acceptance criterion. The Atlas is read back through the notation inAU-09and is byte-equal to its data, so the printer covers it; only the committed bytes are not rewritten. Moving the Atlas would put a new source form into language 1.0.AU-12). A real elaborator for kernel terms would be its own issue.TargetFixtures,ReasoningFixtures,GnafFixtures,GnafCertificates, the extraction adapter'sExtract) are named inAU-07as outputs of a checked comparison against an authority, not hand-owned sources. Inverting them is a rewrite of the conformance crate's oracle layer (about 9,000 lines); I proceeded on the recommendation and did not do it.\semanticdataunder language 1.2): the default (yes, at the end of v0.4). Until thenfmtrewrites it; I will do the refusal as the last change of the milestone.I leave #93 open for your decision on 1 to 3: if you accept them as the closing state, it can close; if you want any of them done, say which and I will open it as its own issue under #27. Two things found on the way, and fixed in this stage: the library identity of a preservation record hashed the library as text and so changed with the notation (found by CI, now over the data form,
AU-06), and AU-10 matched a path by a/suffix that Windows does not have.Generated by Claude Code
afflom commentedon Oct 16, 2026
Closing #93. The DoD summary above left three of its own design calls open "for your decision". They were not decisions; each follows from a requirement of this issue, so this settles them and closes the issue.
\coredata. The DoD says every committed source is in the notation; the acceptance criteria say languages 1.0 and 1.1 are byte-identical. The Atlas is language 1.0 (core schema 1), the notation is schema 2 and is refused under 1.0/1.1 (LLP2003) so that those languages stay byte-identical, so the criterion that cannot be broken without changing a released language governs. Nothing is missing:AU-09reads all 66 Atlas modules back through the notation to their committed data byte for byte, so the printer covers them; only the committed bytes are not rewritten..lex.texalone") is met there. What a person writing a kernel term lacked was names, which 3d gave (AU-12,authored_eq_symm). An elaborator for kernel terms would be a new trusted-path argument, not a part of this issue: if [v0.4] #27 stage 5: certificates A, B, E and the audit modules as typed data, with no Lean text template in the production compiler #89 or [v0.4] #27 stage 6: complete the closed Rust AST so the runtime is generated from the calculus #91 shows a library theorem that cannot be authored without one, that is the issue to open, with that theorem as its evidence.AU-07(TargetFixtures,ReasoningFixtures,GnafFixtures,GnafCertificates, the adapter'sExtract). Each is the output of a checked comparison against an authority (a reference interpreter, the pinned Lean), regenerated only bycheck-calculus --write, which is the discipline the goldens already follow; the gate names them and fails on any other writer. Inverting them is a rewrite of about 9,000 lines of oracle layer that changes no assurance.\semanticdataunder language 1.2 is the one item of this issue that is work, not a decision, and it must come last because it moves the language-1.2 compiler-semantics ID and regenerates every record: it is now [v0.4] Refuse the data form (\semanticdata, \toolingdata, \coredata) under language 1.2: the last change of the milestone #149, in the milestone, ordered after the other regenerating stages.Languages 1.0 and 1.1 stay byte-identical; every other line of the DoD and the acceptance criteria is discharged in the summary above.
Generated by Claude Code