Glitnir 0.1.0

Glitnir 0.1.0

First public release of Glitnir, a notebook format for Lean with a VS Code
extension for reading and checking notebooks as they are written, often by a
coding agent working in the next pane.

A notebook is an ordinary .lean file. Prose goes in /-! … -/ blocks written
in Markdown with $…$ mathematics; everything else is Lean, and the file
builds with standard Lean and Lake.

What it does

• Live reading view. Prose, TeX, definitions and claims render as a
  document next to your editor and update as files are saved, highlighting
  what changed.
• Explicit checking. Check saved file compiles the notebook in a sandbox
  and replays it independently in the Lean kernel. Each claim shows whether it
  is kernel checked, contains sorry or uses additional axioms, with the
  axioms listed. A result goes out of date when the source or its
  environment changes. Check through here checks the file up to one claim.
• Proof steps. Inspect the goals at each tactic step of a claim's proof.
• Linked notebooks. Follow links and the claims a proof uses into other
  notebooks of the same project, inside the same panel. A claim graph shows
  how claims depend on each other.
• Export and history. Export a notebook as a standalone HTML page, or
  browse its git history.
• Extension packages. Optional providers add views, evidence and decision
  procedures. glitnir-forseti, included in this release, adds circuit
  diagrams, simulation evidence and z3-backed decisions for Forseti
  notebooks. A decision only proposes a Lean block; you accept it into the
  file, and the kernel check decides its status.
• Agent skill. The bundled glitnir-notebooks skill teaches coding agents
  such as Claude Code or Codex to write in the notebook style. Install it with
  Glitnir: Set Up Coding Agent.

Install

You need macOS or Linux, VS Code 1.96+, Python 3.12+,
uv, and Lean 4.32.1
through elan with your project's dependencies built. On Linux, checking also
needs bubblewrap; INSTALL.md has the details.

1. Download the assets below and verify them:
   shasum -a 256 -c --ignore-missing SHA256SUMS
   (Linux: sha256sum -c --ignore-missing SHA256SUMS).
2. In VS Code, run Extensions: Install from VSIX… and pick
   glitnir-0.1.0.vsix.
3. Open a Lean file and run Glitnir: Set Up Environment → Install Backend with
   uv. Choose the downloaded backend wheel, or let setup download the
   matching one.
4. Optional: run Glitnir: Install Extension Package… and pick
   glitnir_forseti-0.1.0-py3-none-any.whl for the Forseti features.
5. Run Glitnir: Open in Glitnir.

To try it on real notebooks, clone
forseti-examples, build it with
lake exe cache get && lake build, and open any notebook under examples/.

Assets

• glitnir-0.1.0.vsix: the VS Code extension (universal, macOS and Linux).
• glitnir-0.1.0-py3-none-any.whl: the Python backend the extension runs.
• glitnir_forseti-0.1.0-py3-none-any.whl: the optional Forseti provider package.
• INSTALL.md: installation guide.
• SHA256SUMS: checksums for all of the above.

Limits of this release

• Checking supports Lean 4.32.1 only, the version this release was audited
  against; projects on other versions are refused rather than trusted. Reading
  notebooks works with any Lean version. Support for newer Lean releases is
  next.
• Local macOS and Linux only. Windows is not supported.
• Not yet on the VS Code Marketplace; install the VSIX from this page.
• Checking needs the platform sandbox; Glitnir will not check without it.
• Simulation results are evidence, never proof, and never change a claim's
  status.
• Forseti's iterate evidence needs Python Asgard, which is not publicly
  released.
• Checks of large Mathlib projects take minutes: every check captures the
  project and kernel-replays the notebook. Imported replays are cached between
  checks.

Feedback

This is an early release and there will be rough edges. Please open an
issue for bugs, and report
security problems privately as described in
SECURITY.md.