Glitnir v0.1.3

Glitnir 0.1.3

Faster view drawing, a larger default memory limit for Lean, and a stepped
probability lane in the Forseti plugin.

New

• Views draw without re-running proofs. A notebook's views are drawn with
  theorem and lemma proofs replaced by sorry and examples skipped. If that
  draws nothing, Glitnir falls back to the full notebook. A card drawn this way
  says "Drawn without re-running the notebook's proofs." Evidence runs are
  elaborated the same way. A drawing never grants or changes a claim's status.
• Drawings are saved. They go in a new views section of
  <Notebook>.glitnir.json (at most 4 MiB) and are reused without Lean while
  the source through the directive, the environment and the provider are
  unchanged.
• One Lean run per notebook. A notebook's views from one provider are drawn
  together. Stop on a card drops only that view.
• Reused Lake setup. Views and evidence reuse the prepared Lake setup while
  the environment is unchanged. Checks never do.
• Static export without Lean. SavedNotebook.draw_view uses saved drawings
  as recorded and never writes records. Commit the .glitnir.json to keep a
  gallery Lean-free for views.
• The Mac stays awake while checks, proof steps, views and evidence run
  (macOS idle sleep is held off).
• Forseti: stepped decisions and sample evidence. A discrete-time
  probability lane for driven models: decide breach and expected-energy claims
  by exact arithmetic, emitted as a Lean block the project check judges, and
  sample shock paths as evidence beside a proved bound. Both need a
  forseti-lean build containing Gimle.Forseti.Stepped; until the pinned
  release gains it, the editor reports the missing module.

Changed

• glitnir.memoryLimitMb defaults to 16384 (16 GB), or 2048 MB less than
  the machine's memory when that is smaller. Reaching the limit is now
  explained in the message.

Upgrading from 0.1.2

Update Glitnir from the VS Code Marketplace (or install glitnir-0.1.3.vsix
with Extensions: Install from VSIX…), reload the window and click
Set Up when Glitnir offers to set up its backend. Saved results read as out
of date after the upgrade, because the checker changed; check each notebook
once to bring them current.

Assets

• glitnir-0.1.3.vsix: the VS Code extension (universal, macOS and Linux).
• glitnir-0.1.3-py3-none-any.whl: the Python backend the extension runs.
• glitnir_forseti-0.1.3-py3-none-any.whl: the optional Forseti provider package.
• INSTALL.md: installation guide.
• SHA256SUMS: checksums; verify with shasum -a 256 -c --ignore-missing SHA256SUMS.

Glitnir 0.1.2

Glitnir 0.1.2

Easier setup and one-click upgrades, in preparation for the VS Code
Marketplace.

New

• One-click upgrades. After the extension is updated, Glitnir offers
  "Glitnir was updated to 0.1.2. Set up its backend?". One click downloads the
  matching backend and reinstalls the extension packages you had, such as
  Forseti with z3, each verified against hashes pinned in the extension before
  it is installed. A confirmation lists everything it downloads and installs
  first. Your previous environment is left untouched until the new one works.
  You can also run Glitnir: Set Up Backend for This Version at any time,
  or turn the offer off with glitnir.offerBackendUpdate.
• One-click Set Up. Glitnir: Set Up Environment → Set Up downloads,
  verifies and installs the backend in one step. A downloaded wheel or an
  existing environment are under More Options….
• Install uv. If uv is missing, setup offers Install uv. It shows the
  exact command first and runs it only when you click, in a visible terminal
  with a minimal environment (Homebrew if installed, otherwise uv's installer
  pinned to 0.12.23). Your shell profile is not changed.
• Guided extension packages. Glitnir: Install Extension Package… lists
  the packages Glitnir knows (for now Forseti), offers to download it from this
  release (recommended) or use a downloaded wheel, then asks its own questions,
  such as whether to install z3 for decision procedures.
• Marketplace ready. An icon, listing details and a shorter README with
  separate user and developer guides.

Fixed

• Diagrams in notebooks with many opens. A view could fail with
  "Ambiguous term" when the notebook opened two namespaces declaring the same
  name (such as Gimle.Asgard and Gimle.Asgard.Dynamics, which both have
  Circuit). Provider code now runs in its own scope; only the @view line is
  read in the notebook's scope.
• Failed views and evidence show Lean's whole error, such as its list of
  possible interpretations, instead of only the first line.

Upgrading from 0.1.1

Install glitnir-0.1.2.vsix with Extensions: Install from VSIX… and
reload the window. When Glitnir offers to set up its backend, click Set Up.
From 0.1.2 on, upgrades only need that one click.

Saved results show as out of date once after upgrading, because the checker
changed; check the file again to update them.

Notes

• Checking supports Lean 4.32.1 only; support for newer Lean releases is
  next.
• Notebooks with very large decision proofs may need more than the default 8 GB
  Lean memory limit: raise glitnir.memoryLimitMb to 16384 if a check reports
  "excessive memory consumption".
• On a heavily loaded machine, reading a dependency's git state can time out.
  Results then show as out of date, and diagrams as "may be out of date";
  checking again when the machine is less busy clears it.

Assets

• glitnir-0.1.2.vsix: the VS Code extension (universal, macOS and Linux).
• glitnir-0.1.2-py3-none-any.whl: the Python backend the extension runs.
• glitnir_forseti-0.1.2-py3-none-any.whl: the optional Forseti provider package.
• INSTALL.md: installation guide.
• SHA256SUMS: checksums; verify with shasum -a 256 -c --ignore-missing SHA256SUMS.

Report bugs as issues and security
problems privately as described in
SECURITY.md.

Glitnir 0.1.1

Glitnir 0.1.1

Bug fixes and small features from testing 0.1.0.

Fixed

• Diagrams draw from the project's build. A notebook that imports
  Gimle.Forseti now draws its circuit, model and dynamics views without also
  importing Gimle.Asgard.Visualization.Model. If a module the view needs is
  not built, the card says which lake build to run.
• Long diagrams no longer time out. Views and project inspection run in the
  background with progress and a Stop button, bounded by the check time
  limit instead of a 130-second request timeout.
• Checks wait their turn. A check started while another Lean run is busy
  now waits for it instead of being refused, and has its own Stop.
• Fewer spurious "Out of date" results. Saving an unrelated file, or
  re-saving a file unchanged, no longer marks every saved result out of date:
  only the sources a notebook actually imports count, by content. Anything
  Glitnir cannot read with certainty still counts as changed.
• iterate without Python Asgard is shown as unavailable with the reason,
  instead of failing when run.
• Keyboard shortcuts. The hints and the ? dialog list exactly the keys
  that work, the dialog is readable, and n/p step through the claims that
  need attention (out of date, not rechecked, containing sorry, extra axioms
  or where checking stopped).
• Contents sidebar. Status dots line up inside the column; long names wrap.

Added

• Static export for galleries. glitnir.notebook.static_export.SavedNotebook
  renders a notebook from its saved results without running Lean, clearly
  labelled "Saved results, shown as recorded". See the README section
  "Static export (galleries)".

Upgrading from 0.1.0

There is no automatic update yet.

1. Download glitnir-0.1.1.vsix and run Extensions: Install from VSIX…,
   then reload the window.
2. Run Glitnir: Set Up Environment → Install Backend with uv → Download
   matching backend. 0.1.1 uses a new backend environment.
3. If you use Forseti features, download glitnir_forseti-0.1.1-py3-none-any.whl
   and run Glitnir: Install Extension Package… again. The plugin version
   must match the backend version.

Saved results from 0.1.0 show as out of date once after upgrading, because the
environment fingerprint changed; check the file again to update them.

Notes

• Checking still supports Lean 4.32.1 only; support for newer Lean releases is
  next.
• Notebooks with very large decision proofs may need more than the default 8 GB
  Lean memory limit. Raise the glitnir.memoryLimitMb setting to 16384 if a
  check reports "excessive memory consumption".

Assets

• glitnir-0.1.1.vsix: the VS Code extension (universal, macOS and Linux).
• glitnir-0.1.1-py3-none-any.whl: the Python backend the extension runs.
• glitnir_forseti-0.1.1-py3-none-any.whl: the optional Forseti provider package.
• INSTALL.md: installation guide.
• SHA256SUMS: checksums; verify with shasum -a 256 -c --ignore-missing SHA256SUMS.

Report bugs as issues and security
problems privately as described in
SECURITY.md.

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.