KinoIsabelle

Copy Markdown View Source

Livebook smart cell for Isabelle theories: a CodeMirror editor with Isabelle outer-syntax highlighting and symbol display, checked on demand by a local Isabelle server.

This is an alpha release: expect rough edges and breaking changes.

Installation

Mix.install([
  {:kino_isabelle, "~> 0.1.0-alpha.1"}
])

Isabelle must be installed, with isabelle on PATH or ISABELLE_TOOL pointing to it. Tested with Isabelle2025-2. A logic session without a built heap is built on first use, which can take long. Server cleanup relies on /bin/sh, so Windows is not supported.

Isabelle also needs tar on the PATH of the Livebook runtime; without it, the server fails with Return code 1 from bash script: ".../gnu-utils-.../etc/settings". The NixOS services.livebook service, for example, has no tar on its PATH; add pkgs.gnutar to services.livebook.extraPackages.

Usage

livebooks/demo.livemd walks through the cell.

Add the Isabelle theory smart cell and write theory text. By default the cell generates the header (theory Scratch imports Main begin … end) from the toolbar fields; with header mode "in text" the cell holds a complete theory.

  • Check runs Isabelle on the current text. Errors and warnings appear as lint diagnostics; the panel below the editor shows all messages of the command under the cursor. Nothing is checked while typing.
  • Evaluating the cell returns a KinoIsabelle.Result, shown as Summary / Messages / Errors / Raw tabs, and binds it to the variable in Assign to (result, result2, … by default). An unchanged theory is not checked twice.
  • Symbols such as \<forall> are displayed as ∀. Type \forall, \<forall or an abbreviation like ==> and pick the symbol from the completion list.

The first check of a runtime starts the Isabelle server and the logic session. They are shared by all cells of the runtime and stopped with it. All theories of a runtime are written to one directory, so a cell can import the theory of another cell that was checked before.

Without the smart cell:

{:ok, result} = KinoIsabelle.check(~S(lemma "\<forall>x. x = x" by simp), imports: ["Main"])

Development

mix test                          # includes Isabelle integration tests when isabelle is found
cd assets && npm install && npm test
npm run build                     # rebuilds lib/assets/cell/build (committed), including
                                  # THIRD_PARTY_LICENSES.txt for the bundled npm packages
mix kino_isabelle.gen_syntax HOL  # regenerates priv/keywords.json and priv/symbols.json

The keyword table is generated for one logic (HOL); keywords that other sessions add are not highlighted. After regenerating it, rebuild the assets.

License

MIT, see LICENSE. The bundled editor code (CodeMirror and its dependencies, all MIT) comes with its licenses in lib/assets/cell/build/THIRD_PARTY_LICENSES.txt.