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.