LeanTeX

Include Lean 4 source, diagnostics, and proof states in LaTeX PDFs. Use an existing local Lean project or check small snippets remotely through Lean Web.

Documentation · Example source · Earlier v2.5 PDF

Get started

You need Python 3.9+ and a TeX distribution with latexmk, minted, and XeLaTeX or LuaLaTeX.

git clone https://github.com/rgrossharv/LeanTeX.git
cd LeanTeX
python3 -m venv .venv
source .venv/bin/activate
python -m pip install -e ".[remote]"
leantex build examples/quickstart.tex --backend remote

The CLI supplies its bundled .sty files to TeX; a separate style installation is unnecessary. PDF builds enable shell escape for minted, so use trusted TeX sources. Remote mode sends the extracted Lean source to the selected server; LaTeX and PDF compilation stay local.

\documentclass{article}
\usepackage[onefile]{leantexv2}
\begin{document}

\begin{minted}[label=successor]{lean}
#check Nat.succ
example : 1 + 1 = 2 := by decide
\end{minted}
\leantexoutput{successor}

\end{document}

Hidden, output-only snippets use \leantex{...}. Legacy v2 blocks use \begin{lean} ... \end{lean}, with the closing command on its own line. The onefile option shares declarations; without it, snippets have separate namespaces. Mixed minted blocks, hidden snippets, and Lean environments retain their document order.

Local checking

leantex build paper.tex --project-root /path/to/existing/project

Local is the default. LeanTeX reads the existing Lake manifest and compiled libraries, then starts the already installed Lean binary directly. Set up and build dependencies yourself before using this mode. For a custom installation, set LEANTEX_LEAN=/path/to/lean.

Builds never provision a workspace, invoke an elan download shim, run lake update, fetch Mathlib, or copy toolchains/dependencies. Missing installations produce an error with a remote-backend alternative. Custom Lake scripts and environment variables are not executed; projects requiring these should prepare their environment before invoking LeanTeX.

Remote checking

leantex projects
leantex build paper.tex --backend remote --remote-project MathlibDemo

The adapter uses Lean Web's projects endpoint and WebSocket editor protocol, with Lean's textDocument/waitForDiagnostics, $/lean/plainGoal, and $/lean/plainTermGoal requests. It produces text diagnostics and plain proof states, not screenshots or interactive widgets. This is an editor protocol, not a stable hosted rendering API; server availability and project versions can change. Public Lean Web is intended for small examples. For larger work, use a local project or your own Lean Web instance:

leantex build paper.tex --backend remote \
  --remote-url https://your-lean-web.example --remote-project YourProject

Remote checking cannot access your local Lean modules. Select a project containing your imports. The remote cache is keyed by server, project, extracted source, and infoview mode; use --refresh after a remote project updates. There is no automatic fallback that uploads local code or installs dependencies.

Set LEANTEX_BACKEND, LEANTEX_REMOTE_URL, LEANTEX_REMOTE_PROJECT, or LEANTEX_PROJECT_ROOT to persist a choice in your shell/editor environment.

Proof states and output

\leantexconfig{successor}{infoview=lines:4,outsize=footnotesize}
\leantexoutput[Optional heading]{successor}
\totalinfoview

Mode	Behavior
auto	Compact state from the last nonblank code line (default).
lines:N	Final state, with at most N displayed state lines.
full	Query each nonblank code line in the snippet. Slower; opt in when needed.
goals	Final tactic goal and diagnostics.
off	Diagnostics only, with no goal queries.

Override all snippets from the CLI with --infoview auto\|full\|goals\|off. \totalinfoview reuses collected results rather than scanning the file again. Display names use letters, digits, :, _, and -; names must be unique. codesize, outsize, and textsize accept standard TeX font-size commands.

LeanTeX's output uses plain, page-breakable verbatim text, without running Pygments for diagnostics. It keeps font changes and Unicode fallbacks inside listings. Use \leantexsetfont{JuliaMono} to select a font with broad Lean symbol coverage. \leantexsetoutputstyle{...} accepts fvextra verbatim options; \leantexsetcodestyle{...} accepts minted options.

Fast builds and editors

leantex build paper.tex --backend remote --no-latexmk
leantex watch paper.tex --backend remote
leantex build paper.tex --backend remote --strict --timeout 180
leantex doctor

Each build uses one Lean language-server session. Results are cached under .leantex/<document>/; each main TeX file gets its own <document>.leantex.generated.tex. Prose edits reuse Lean results, while generated files keep their timestamps when unchanged. Local cache keys include the toolchain binary, manifests, user Lean sources, and imported compiled-module stats. --refresh bypasses the cache; LEANTEX_NO_CACHE=1 disables it.

Ordinary \input and \include trees (including \includeonly) are read in document order. Watch mode tracks these inputs and user Lean sources. This is a static parser, not a TeX interpreter: commands generated by macros, conditional inclusion, custom import packages, and \inputminted are not expanded. Use explicit Lean blocks in ordinary TeX inputs. Hidden \leantex{...} bodies must have balanced braces; use the lean environment for arbitrary Lean strings and comments.

Build errors/timeouts are reported and never cached as successful empty output. --strict returns a failure status for Lean errors, after generating the diagnostic output. The default allows intentional Lean errors in teaching examples.

For a separate TeX editor:

leantex install-tex                     # styles only
leantex install-tex --latexmk-hook      # also opt in to a ~/.latexmkrc hook

The CLI skips a duplicate check in that hook during its own PDF build. Regenerate output after updating from the earlier version. Old root-level generated files can be removed manually once the new outputs work. The version1 and version2 branches preserve the older releases.

Development

python3 -m unittest discover -s tests -v
python3 -m build

The unit tests use fake servers and temporary files; they never install or run Lean. The optional scripts/full_test.sh builds a temporary copy of the small example using the selected backend, preserving checked-in example PDFs. CI checks the Python suite, site links/metadata, and bundled wheel styles without Lean downloads.

Public domain dedication via The Unlicense.