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.