Roadmap

Purpose

ExactTeX gives a writer information about the reliability of a document before they inspect the PDF.

It is a one-directional superset of LaTeX. Every valid .tex file is valid ExactTeX input, while a .xtex file may contain constructs that plain TeX cannot process. LaTeX remains the typesetting backend and the artifact submitted to journals.

The project combines:

• diagnostics stated using author-declared entity names;
• revisions stored as structured data in the document format;
• faithful transport of existing LaTeX;
• checked references, citations, figures, tables, paths, lengths, and revision identifiers;
• editor operations over one project-wide document model.

Typed document languages, semantic LaTeX annotations, and LaTeX language servers already exist. The admissible claim is that this combination is not assembled. See PHILOSOPHY.md §3 and §7.

Correctness properties

A. Transport

For any input byte sequence u containing no ExactTeX constructs:

emit(parse(u)).tex == u
check(parse(u)) produces no hard errors

The first comparison is byte equality, not textual or Unicode equivalence. Line endings, encodings, comments, whitespace, and opaque macro bodies must remain unchanged.

A renamed .tex checking clean means that ExactTeX emits no hard diagnostics of its own. It does not mean that the input compiles successfully under TeX.

A transport test fails if

cmp input.tex build/input.tex

reports any difference.

B. Typesetting equivalence

For every document d that passes checking:

render(tex(emit(d).tex)) == render(tex(emit(erase(d)).tex))
tex(emit(d).tex).status == tex(emit(erase(d)).tex).status

render uses a pinned TeX engine, removes declared volatile metadata, rasterizes pages under fixed settings, and compares page structure and pixels under a declared tolerance.

The property fails if adding a valid annotation changes a normalized rendered pixel, or changes a successful TeX invocation into a failed one.

ExactTeX uses erasure, not injected assertions, wrapper environments, or support packages. Such injection could collide with packages or catcodes and would violate this property.

Project and output structure

A project is located by walking upward to the nearest xtex.toml. A project may declare several document roots.

A normal build emits one .tex file for every .xtex file and mirrors the source layout under build/:

paper/main.xtex                 ->  build/paper/main.tex
paper/sections/model.xtex       ->  build/paper/sections/model.tex
paper/appendices/proofs.xtex    ->  build/paper/appendices/proofs.tex

The normal emitter does not flatten a project into one file. Flattening would inline \input or \include, thereby transforming LaTeX the author did not touch and breaking transport byte identity.

--flatten is an explicit opt-in for single-file journal submission. Its diagnostics and documentation must state that flattened output is a conversion artifact and does not satisfy transport byte equality.

Paths in @import, src, and similar fields resolve relative to the file containing the field. Imported symbol tables merge at project scope, while emission preserves file boundaries.

Compiler architecture

The implementation is in Rust. Native and WebAssembly builds use the same core crates.

                xtex-core   the compiler (~10,000 lines)
               /    |    \
        xtex-cli  xtex-lsp  xtex-wasm
        terminal   editor    browser

Every door links xtex-core statically and carries its own copy; none links another door. Anything two doors would share moves down into the core — project, blame, the JSON renderers all made that move — so “the doors answer alike” holds by construction, and the parity suite checks it rather than provides it. The one consequence worth remembering: when the core changes, the three doors recompile together in this repository, but the published .wasm stays at its tagged commit until the next release — which is why the release manifest names the commit.

The measurement instruments (tests/corpus/*.py, the render harness) deliberately do not link the core: they drive the binary through its public interface, measuring what a user touches rather than what the library promises.

All source access, project discovery, output storage, bibliography access, and TeX invocation sit behind I/O traits. The compiler core must not contain assumptions about host paths, process spawning, current directories, or direct filesystem access.

WebAssembly is a first-class output alongside the native binary. Rust makes the additional target a small architectural extension, provided that I/O is isolated from the core. It is the route to a browser surface without a compile server. TeX already runs in browsers through WASM: SwiftLaTeX does so, and TeXlyre-BusyTeX supports TeX Live 2026 with pdfLaTeX, XeLaTeX, and LuaLaTeX.

Two front doors

Both inputs converge on the same Document model:

1. Native front door — parses explicit ExactTeX syntax: @id, @ref, @cite, @import, typed blocks, revision constructs, and delimited raw-LaTeX escapes.
2. LaTeX front door — shallow parsing: recognizes safe boundaries, records selected declarations, and represents everything else as opaque source spans.

Neither front door owns resolution, checking, emission, diagnostics, or editor behavior.

Five compiler stages

1. Parse and preserve

   • Load immutable byte buffers through the I/O trait.
   • Select the native or shallow-LaTeX front door.
   • Produce a shared Document with spans on every node.
   • Preserve unmodelled bytes in Opaque nodes.
   • Record ParseConfidence::{Structured, OpaqueBalanced, OpaqueToEof}.

2. Resolve

   • Discover the nearest xtex.toml.
   • Resolve literal imports and file-relative paths.
   • Merge declarations into a project-wide symbol table.
   • Load successfully parsed bibliographies.
   • Detect duplicate entities and orphaned revision metadata.

3. Check

   • Apply entity-class consistency and explicit-construct validation.
   • Produce hard errors only from explicit ExactTeX constructs.
   • Treat ordinary LaTeX as UnknownOpen (?O), consistent with every entity class.
   • Keep raw-LaTeX observations advisory behind --strict-tex.
   • Calculate checked-versus-opaque coverage. Where an author annotates fully, the useful signal is a coverage drop — something entered the document that the compiler does not understand — rather than an absolute threshold.

4. Emit

   • Erase annotations and lower native constructs to LaTeX.
   • Copy opaque spans directly from immutable source buffers.
   • Emit the mirrored build/ tree, one .tex per .xtex.
   • Optionally produce explicitly non-transporting --flatten output.
   • Write source-map segments while output bytes are produced.

5. Attribute and report

   • Parse TeX file-line diagnostics.
   • Map output byte offsets back to source spans.
   • Assign blame as AuthorLatex, XtexNative, XtexGenerated, or unresolved.
   • Translate supported visual failures using declared entity names.
   • Render one diagnostic model as human-readable text, JSON, and LSP diagnostics.

Opaque node

The opaque node is the transport boundary:

struct Opaque {
    source: SourceId,
    span: Span,
    confidence: ParseConfidence,
}

Span indexes an immutable source byte buffer. It does not hold a decoded and re-encoded copy. Emission copies the indexed byte slice directly.

Opaque content is never normalized, expanded, structurally checked, or rejected because of unfamiliar LaTeX. Searches for \label, \ref or \cite inside opaque content may produce advisory information only.

Source map

Each emitted file has a corresponding map such as paper.xtexmap containing:

enum OriginKind {
    AuthorLatex,
    XtexNative,
    XtexGenerated,
}

struct MapSegment {
    output_start: u32,
    output_end: u32,
    origin: OriginId,
}

The map also records SHA-256 fingerprints of input and output; ordered, non-overlapping output segments; source-file identities; and source spans with line indexes.

A diagnostic without a supporting map segment receives blame: unresolved. The compiler must not guess an origin.

Parser hazards

The shallow LaTeX parser preserves rather than rejects. After entering OpaqueToEof, it recognizes no further ExactTeX constructs.

Construct	Parser behavior	Falsifying observation
\verb, \verb*	First non-space byte is the delimiter; scan literally. A missing delimiter forces OpaqueToEof; no delimiter is synthesized.	Bytes inside the literal are parsed as ExactTeX, or an unterminated literal is repaired or rejected.
verbatim, lstlisting	Copy raw lines through the exact environment terminator. Extra verbatim environment names come from xtex.toml.	A marker inside the environment becomes a ExactTeX node, or any contained byte changes.
\catcode	Do not evaluate. OpaqueBalanced for the remaining group only if corpus evidence establishes a reliable boundary; OpaqueToEof at top level.	Parsing resumes past a boundary the corpus shows can be changed by expansion.
\makeatletter, \makeatother	Permit @ in control-sequence names within a matched pair. An unmatched opener makes the remainder opaque.	A control sequence in the pair is split at @, or native syntax is recognized after an unmatched opener.
\newenvironment and variants	Parse only the declaration shell needed to locate arguments. Bodies stay opaque; no grammar is inferred from them.	A marker in a definition body is treated as an active construct.
\newcommand, \def, \edef, \gdef	Record the declared control-sequence name and arity. Body stays opaque and is never expanded.	The body is expanded, normalized, or counted as checked content.
\csname … \endcsname	Preserve as an opaque balanced node. Do not infer the generated control-sequence name.	The generated name enters the symbol table as a definite declaration.
\input, \include	Record an opaque project edge. Do not splice file contents into the byte stream during parsing or normal emission.	Normal output contains inlined imported bytes.
\if…, \else, \fi	Preserve every branch as opaque. Do not evaluate the condition.	Only one branch is retained, or constructs in either branch produce hard errors.

Checking and diagnostics

Hard errors are limited to explicit ExactTeX constructs:

• duplicate explicit identifiers;
• unresolved @ref;
• a reference requiring a known entity class that differs from the target’s known class;
• unresolved files declared by typed constructs;
• @cite keys absent from a bibliography that was read successfully;
• unsupported length units, or percentages outside the accepted range;
• orphaned revision identifiers;
• overlapping or unbalanced revision constructs.

Ordinary \ref, \cite, unfamiliar macros, failed inference, and comparisons involving ?O do not produce hard errors. Optional raw-LaTeX findings are labelled advisory, require --strict-tex, and do not change the process exit code.

Structural table checks must account for constructs such as \multicolumn; a simple token count is not sufficient.

Revision model

The source format contains:

@add(id) { text }
@del(id) { text }
@sub(id) { old -> new }
@note(id, on=entity-id) { text }

Metadata such as author, status, and discussion thread lives in a sidecar such as paper.xtex.review, keyed by revision identifier.

The initial model forbids overlapping changes and requires balanced content. A substitution is atomic when accepted.

Emission modes, one document each:

• --original — the document before any revision;
• --final — the document with every revision applied;
• --marked — every change visible, for reading rather than submitting.

There is no status that makes --final render two ways, which is why accepting is a source rewrite rather than a stored state. Accepting keeps the proposed text and removes the construct; rejecting keeps the original text and appends what it removed to the sidecar’s history, so a rejected paragraph is still recoverable. xtex check reports a sidecar record whose construct is gone as a hard error, and a construct whose record is gone as an advisory — the file is authoritative for content, the sidecar only for attribution. See docs/revisions.md.

Phases

Phase 0 — Gather what Phase 1 needs

Two write-ups, no compiler code. Neither judges the project; both are input to the grammar and to the diagnostics:

• rewrite a section of a published paper in the specified syntax, declaring every referenceable thing in it, and record what the language does not let you name. The output is that gap list, not a percentage. Every diagnostic in this project names something the author declared; what cannot be declared is what will never get a good error message. This does not judge the notation, which is a settled design decision;
• run a minimal defective example for every error class through tectonic, chktex, chklref and texlab, and record what each one reports. The question here is where the messages have to be better than what LaTeX already prints, and which classes have no existing message at all — not whether the checks are worth having.

Done when both write-ups exist: the list of things the language cannot yet name, and the table of what existing tools already report. Both feed Phase 1 — the first says what the grammar has to cover, the second says where the error messages need to be better than what LaTeX already prints.

Phase 1 — Freeze the language contract

Write the formal grammar, lexical boundaries, explicit hard-error policy, erasure rules, review-mode semantics, and representative valid and invalid examples.

Revisions are settled: the content of a change lives in the .xtex, the author and conversation live in a .xtexrev beside it, accepting rewrites the source, and there is exactly one --final per document. See docs/revisions.md.

The package-synthesis conflict is settled: needs is not a field, packages are written by the author in the preamble, and a typed block lowers to the LaTeX its fields describe and nothing else. See docs/decisions/0001.

Done when every construct has a boundary that can be found without looking ahead past end of line, and no two examples in the spec demand different output for the same input.

Phase 2 — Build the native language

Immutable sources, native parsing, the shared document model, project discovery, resolution, checking, bibliography access, coverage, revision constructs, mirrored emission, source maps, and human/JSON diagnostics. Raw LaTeX is available only through its explicit delimited escape in this phase.

Done when a real paper parses, checks, emits into a mirrored build/ tree and compiles, without needing the raw escape for ordinary figures, tables, sections and references — and every diagnostic carries a source span and a blame value.

Phase 3 — Add the LSP and the WASM/browser surface

The language server and the WebAssembly build are done. What remains — the browser surface that supplies a multi-file project to the module, and the choice of a TeX compiled to WebAssembly, which nobody has verified — is Phase 6, because it turned out to be a phase rather than a loose end. See docs/wasm.md and docs/lsp.md.

Diagnostics, hover, project-wide completion, definition lookup, safe rename, and macro declaration information through the LSP. Compile the same core to WebAssembly and connect it to browser-provided source and output stores.

Done when rename across the whole project leaves no stale reference, the LSP and the CLI report the same diagnostics for the same input, and the WASM build needs no filesystem or process access in the core.

Phase 4 — Add the LaTeX on-ramp

Shallow LaTeX parsing, parser quarantine, opaque transport, selected macro declaration recording, multi-file preservation, and TeX-log attribution. Assemble licensed corpus files with declared provenance plus synthetic files for every parser hazard. Set quarantine thresholds before measuring the corpus.

Done: tests/corpus/ holds the thresholds, the tooling and ten hazard fixtures. Real documents are referenced by fingerprint rather than vendored, because their licences are not ours to grant. The baseline was taken and is recorded with the reason it does not yet mean what it appears to.

Done when every corpus file transports byte-for-byte with no per-file special case, and quarantine stays rare enough that real documents still have room to annotate.

Phase 5 — Qualify the guarantees

Fuzzing for lexical boundaries and quarantine transitions, byte-transport property tests, annotation insertion generators, deterministic TeX reruns, normalized raster comparison, and native/WASM conformance fixtures.

Done when the suite is green: no byte differs on transport inputs, no valid annotation changes a rendered page or a build status, and native and WASM agree on the shared fixtures.

Phase 6 — Make the WebAssembly module something a product can be built on

Phase 3 produced a WebAssembly build. This produces a WebAssembly API, and the difference was found by running the compiler over a real Springer monograph: the module’s three entry points each take one file, under a fixed name, while everything that makes the compiler worth using is multi-file — @import, the label inventory that spans \include, bibliographies, and rename, which is valuable precisely because it reaches the whole project.

The host supplies the project on every call, whole. That was decided against the alternative of calling back into the host per file, on two grounds: the monograph is 388 KB across 20 files and checks in 71 ms including twenty process starts, so there is nothing to save by reading lazily; and WebAssembly imports are synchronous, so the shape that appears to serve a file arriving over a network is the one that serves it worst.

Everything the features need already exists in xtex-core and is exercised by the language server. This phase is translation, not new behaviour — with one exception worth naming: the browser currently cannot reach texlog or map_emitted_diagnostic, so a product built on the module today would show ! Undefined control sequence and nothing this project exists to add.

The phase ends with the module published as a versioned artefact, which is what lets the browser product live in its own repository. That separation follows from licensing, not size: the browser TeX engine under consideration is AGPL-3.0 while this project is MIT, and a licence boundary cannot be undone once it is in a repository’s history; and this workspace holds four packages in Cargo.lock and no external dependencies, a promise a package.json in the same tree would quietly weaken.

Done when a project of several files produces through WebAssembly exactly what the CLI produces for the same project on disk — including its failures — and a separate repository can build against the published artefact using nothing but docs/wasm.md.

Explicitly out of scope

• A TeX interpreter or typesetting engine.
• Full TeX macro expansion.
• Evaluation of catcodes or conditionals.
• Replacing LaTeX as the artifact of record.
• Converting arbitrary LaTeX into a normalized ExactTeX representation.
• Hard errors derived from ordinary unannotated LaTeX.
• Scanning opaque content and presenting matches as checked facts.
• Wildcard imports.
• Non-literal include or bibliography discovery, unless later evidence justifies it.
• Entity-specific blocks beyond demonstrated needs; @id remains the fallback.
• Overlapping revision changes in the initial revision model.
• A review UI before the source and sidecar data model is stable.
• Multiple TeX engines until the pinned-engine qualification path passes.
• Reuse of texlab’s GPL parser in the MIT-licensed compiler.
• Claims of priority, uniqueness, or superiority.

Not yet verified

The compiler, the CLI, the LSP and the WebAssembly module exist and their suites run in CI; the formal grammar is written; transport (property A) and clean checking are measured against the corpus in tests/corpus/RESULTS.md. What remains open, honestly stated:

• Typesetting equivalence (property B) is unmeasured. That annotating a document moves no pixel of its typeset output requires compiling each corpus document twice and comparing rasters; the raster normalization and its noise floor have not been established.
• The WebAssembly artefact’s only downstream consumer today is a private repository; no public integration has exercised the published contract yet.
• Group-local quarantine after \catcode remains unestablished; the shipping behaviour is the safe fallback, OpaqueToEof (grammar §confidence).
• Literature outside the languages and indexes already searched remains outside the novelty-check boundary.
• Any new external capability or priority claim requires a fresh check against sources opened for it.