span

KO | EN

gitlite — search

#javascript #python #hacktoberfest #react #ai #typescript #llm #go #golang #android #machine-learning #rust #deep-learning #linux

(★ 18)

No description available.

span Latest Version Download

Download Latest Version (.zip)

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

# span

`span` bridges a LaTeX mathematics paper and its Lean 4 formalization. It
indexes raw Lean declarations, parses the paper's standard `\label{...}` commands, and
uses a **ledger** (`build/<paper>.lea`, JSON) to align paper objects
and Lean declarations. The ledger records, for every object, which Lean declarations realize it and whether they are formalized.

Optional `span:` comments in Lean can provide hints, but they are not required:
the core model is raw Lean facts + paper objects + a curated ledger. For
dependency graphs, `span` derives edges deterministically from the labeled
LaTeX, the Lean source/build, and the ledger.

It is both a CLI and a Python library.

## Project layout it expects

```
<project>/
  latex/   main.tex            # paper, indexed by \label{...}
  lean/    *.lean              # Lean source; span indexes declarations directly
  build/   <paper>.lea         # curated/generated ledger (+ spines)
  span_notes.json             # optional per-entry notes, keyed by align id
```

`span` auto-detects the project root (the nearest ancestor with `latex/` and
`lean/`); override with `--project/--paper/--lean-source/--out`.
`--paper` and `--lean-source` are repeatable. With no explicit
Lean input, `span` indexes `lean/` directly and, when `build/<paper>.lea`
already exists, uses that ledger as the curated alignment.

## CLI

```
span build              # reconcile -> build/main.lea (+ spines) and run checks
span init-ledger        # create a starter ledger from paper ids and raw Lean declarations
span build --lean-source lean
                        # preferred: index raw Lean declarations directly
span build --lean-source lean --ledger build/main.lea
                        # validate/update using an existing curated alignment ledger
span build --full-lean-coverage
                        # include every unaligned raw Lean declaration as a lean half-span
span build --paper latex/main.tex --paper latex/appendix.tex
                        # reconcile a corpus of multiple labeled paper roots
span build --latex      # also run a pdflatex compile check (C8)
span build --decls      # also check named lean decls exist in source (C13)
span check [--strict]   # run the verification suite; nonzero exit on errors
span check --decls      # add C13: cross-check ledger decl names against the Lean source
span compare --ledger build/main.lea
                        # print the curated paper<->Lean alignment table
span compare --against build/main.lea   # diff the entry set against a saved ledger
span stats [--json]     # statistics from the paper, Lean spine, and alignment
span graph --paper-facing --render --dot build/deps_statements.dot
                        # paper-facing Graphviz graph: one node per paper object,
                        # with native edges from LaTeX + Lean + ledger
span graph --paper-facing --edge-provenance build/edges.json --dot build/g.dot
                        # also write a machine-readable edge provenance audit
span graph --edge-source lean --dot build/deps_lean.dot
                        # Lean-facing graph from elaborator dependencies
span graph --edge-source lean --lean-filter ledger --dot build/deps_aligned.dot
                        # Lean-facing graph restricted to ledger-owned declarations
span order              # paper statement order vs a dependency-respecting order (C12 detail)
span lean | span paper  # emit either spine as JSON
span vocabulary [--json] # print the controlled vocabulary: kinds, statuses, checks
span --version
```

## Minimal Example

The directory `examples/one_theorem/` is a complete ledger-first
project aligning a human-readable proof of `1=1` with a Lean 4 formalization.

```
examples/one_theorem/
  latex/main.tex
  lean/One.lean
  build/main.lea
```

From that directory, the normal workflow is:

```bash
span build
span check
span compare
span stats
span graph --paper-facing --dot build/one.dot
```

To initialize the ledger from the paper and raw Lean source:

```bash
rm build/main.lea
span init-ledger
```

The paper label names the paper object:

```tex
\begin{theorem}[One equals one]\label{thm:one}
\(1=1\).
\end{theorem}
```

The ledger supplies the Lean declaration:

```json
"lean_decls": ["One.one_eq_one"]
```

For corpus builds, the output ledger is `build/corpus.lea` unless `--out` points
elsewhere. The paper side is the coproduct of the input paper summands, the Lean
side is the coproduct of the input Lean summands, and the ledger records the
alignment span between them. If a ledger entry needs to point to a Lean object
whose id is duplicated across Lean summands, qualify the ref with the source path
recorded by `span`, the basename, or the basename stem. Ambiguous unqualified
refs are reported by C15 as ambiguity across coproduct summands.

## Ledger-first Alignment

Paper labels identify paper objects:

```tex
\begin{theorem}[One equals one]\label{thm:one}
...
\end{theorem}
```

The ledger supplies the Lean declarations:

```json
{
  "id": "align:one",
  "kind": "theorem",
  "title": "One equals one",
  "paper_ids": ["thm:one"],
  "lean_decls": ["One.one_eq_one"]
}
```

`span check --lean-source lean --ledger build/main.lea` then deterministically
checks that the named paper objects and Lean declarations still exist and remain
kind-compatible. The ledger can be created by hand, by an LLM-assisted matching
workflow, or by `span init-ledger` and editing it.

## Graphs

`span graph` writes Graphviz DOT.  To make a PDF, run Graphviz separately:

```bash
span graph ... --dot build/graph.dot
dot -Tpdf build/graph.dot -o build/graph.pdf
```

With `--render`, statement labels are typeset with LaTeX into cached PNG files
under the output directory.  This needs a local TeX installation and either
`dvipng` or a PDF-to-PNG tool supported by `span`.

### Paper-facing graphs

The paper-facing graph is the figure-style graph:

```bash
span graph --paper-facing --render \
  --paper latex/main.tex \
  --ledger build/main.lea \
  --dot build/deps_statements.dot \
  --edge-provenance build/deps_statements_edges.json
dot -Tpdf build/deps_statements.dot -o build/deps_statements.pdf
```

It has one displayed node per ledger owner:

- ordinary aligned entries are owned by their first `paper_ids` label;
- curated Lean half-spans are owned by their ledger entry id;
- paper half-spans are shown as orange nodes;
- Lean half-spans are shown as grey nodes.

When the project uses raw Lean source (the default), `--paper-facing` defaults
to `--edge-source native`.  Native edges are derived deterministically from the
labeled LaTeX paper, the Lean source/build, and the ledger.  No LLM,
external graph file, or hand-written edge list is used.

The native edge semantics are:

- **solid statement dependency**: Lean elaborator dependencies between
  ledger-owned declarations, projected through the ledger.  If a declaration
  owned by paper object `P` depends on a declaration owned by `Q`, the graph
  gets `Q -> P`.
- **dashed proof dependency**: explicit LaTeX proof structure, including
  references inside `proof` environments, references feeding inline labeled
  proof objects, inline labels inside proofs, and simple summary sentences such
  as "Theorem P follows from Q and R".
- **orange dashed forward proof dependency**: a dashed proof dependency whose
  prerequisite appears later in paper order.  These are allowed: they record
  exposition order, not a statement-level circularity.

By default, native paper-facing graphs use a transitive display reduction, so
redundant cover edges are omitted from the drawn figure.  The JSON written by
`--edge-provenance` records every raw edge, whether it was displayed,
transitively reduced, or suppressed by display policy, together with Lean
declaration pairs or LaTeX line/rule provenance.

The Lean-derived edges are statement/formal dependencies.  Lean theorem proof
terms are not retained in imported `.olean` files, so theorem proof-body
dependencies are supplied by explicit LaTeX proof references rather than by
attempting to recover proof terms from Lean artifacts.

The display policy is deliberately separate from edge derivation.  By default,
span suppresses formal edges into inline definition anchors, since prose labels
for definitions are usually anchors rather than separately displayed
definition environments.  Project-specific section suppression belongs in the
ledger, not in span code:

```json
"graph": {
  "paper_facing": {
    "display_policy": {
      "suppress_formal_edges_from_sections": ["Formal verification"],
      "suppress_formal_edges_into_inline_definition_anchors": true
    }
  }
}
```

`suppress_formal_edges_from_sections` removes formal display edges from objects
in the named sections into objects outside the same section.  This is useful for
certification or implementation-wrapper sections whose low-level formal
dependencies would otherwise clutter a paper-facing mathematical figure.  The
raw suppressed edges remain visible in the `--edge-provenance` JSON audit.

Use `--edge-reduction none` to disable the transitive display reduction.

`span build` and `span check` report C12 as a warning if native Lean dependency
querying cannot run, for example in a tiny non-Lake example.  `span graph` and
`span order` require that query to succeed because their primary output is the
dependency graph/order itself.

### Lean-facing graphs

The Lean-facing graph keeps Lean declarations as graph nodes.  With raw Lean
source, `--edge-source lean` asks Lean for elaborator dependencies among the
selected declarations:

```bash
span graph --edge-source lean --dot build/deps_lean.dot
dot -Tpdf build/deps_lean.dot -o build/deps_lean.pdf
```

To inspect only declarations named by the ledger, use:

```bash
span graph --edge-source lean --lean-filter ledger \
  --dot build/deps_lean_aligned.dot
dot -Tpdf build/deps_lean_aligned.dot -o build/deps_lean_aligned.pdf
```

Use `--edge-reduction none` to keep all derived Lean edges, or leave the
default `auto` behavior to transitively reduce Lean-derived display graphs.

## Optional Lean Source Hints

Direct Lean mode also understands inert `span:` comments immediately before
declarations. These are optional hints; they are not required when a ledger
supplies the alignment.

Single-line form:

```lean
-- span: id=thm:one kind=theorem title="One equals one"
theorem one_eq_one ... := by
  ...
```

Doc-comment form:

```lean
/-- span:
id=thm:one
kind=theorem
title=One equals one
statement=The distinguished object equals itself.
-/
theorem one_eq_one ... := by
  ...
```

Supported keys for native workflows are `id`, `kind`, `title`, and
`statement`. The declaration itself supplies the fully-qualified Lean
declaration name. If no `span:` comment is present, the declaration is still
indexed under its fully-qualified name.

## Library

```python
import span
lean    = span.parse_lean_sources(["lean"])
paper   = span.parse_paper("latex/main.tex")
entries = span.reconcile(lean, paper)
ledger  = span.build_ledger_dict(lean, paper, entries, "main.tex", "lean")
for f in span.run_checks(lean, paper, entries):
    print(f.severity, f.code, f.message)
```

Recognized paper/Lean spine kinds are:

```
definition, lemma, theorem, proposition, corollary, claim, conjecture,
remark, example, notation, convention, assumption, axiom, constant
```

`constant` is normally a paper-side label kind.  Run `span vocabulary` for the
full compatibility table, span statuses, and check families.

## Alignment Model

The span tool is, at the top level, the one span that
bridges the paper side and the Lean side:

```
Paper  <---  span  --->  Lean
```

That global span is assembled from one small span per aligned concept. The
structure is self-similar, not a name clash: you *run* `span` (the tool) and
*read* spans (the entries) in the **ledger** (`.lea`) it writes.

- **Each ledger entry is an alignment span**: an apex (the aligned concept) with
  a *paper leg* and a *lean leg*. The canonical `span_status` is the span's
  shape: `coherent`, `paper_half`, `lean_half`, or `incoherent`.
- **The checks are grouped by alignment family**, shown in every report:
  *object* (well-defined and kind-preserving: C1-C4, C8, C10, C13),
  *coherence* (native dependency order: C12), *coverage* (paper and Lean
  half-spans: C6, C7), and *fiber* (shared formalizations and fan-out: C5).
- **Fan-out is a fiber** (`largest_fiber` in `span stats`), and
  `build`/`compare`/`stats` print an **alignment verdict** naming each
  obstruction.

## Checks

C1 id uniqueness · C2 dangling refs · C3 kind compatibility · C4 stated results
in labeled environments · C5 duplicate/shared formalizations · C6 lean half-span
coverage · C7 partial formalization · C8 LaTeX compile check · C10
compatible-kind notes · C12 statement order is a linear extension of native
Lean statement dependencies lifted through the ledger · C13 (opt-in, `--decls`)
named ledger declarations exist in the Lean source with a matching kind · C15
corpus id ambiguity/source qualification. See `CHECKS.md`.

C13 is the strongest *machine-checkable* paper<->Lean consistency check that
needs no proof-assistant run and no LLM: a heuristic source scan confirms every
named declaration exists and that a definition node is backed by a `def` (a
theorem node by a `theorem`/`lemma`).

Native graph generation runs Lean (`lake env lean`) to traverse the constants
each selected declaration's *statement* (type) references, through
project-internal helpers and stopping at other selected declarations.  This
builds the statement/formal dependency edges used by `span graph --paper-facing`
and `span graph --edge-source lean`.  Proof-only theorem dependencies are not
available from imported oleans, so paper-facing proof edges are derived from
explicit LaTeX references instead.

These automated checks cannot verify that the two statements *mean* the same
thing -- that semantic faithfulness is the specification gap, which only a human
or (heuristically) an LLM can judge.

span

span Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

span

span Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

Download README