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.