Setup and release status

Try it yourself

Source is in the Definograph GitHub repository. Build the reader and its controller locally; no qualified installer or Marketplace release is provided.

Follow the repository’s README and the local setup guide. Keep the reader, native engine and editor controller at the same source revision. The figures on this site are recordings with stated dates, so a newer checkout can look different.

The lessons and figures describe Definograph at its revision of 2 October 2026. The current source differs in three ways that change the steps of the lessons. It opens a statement with one nested drawing of the whole statement, in place of the outline beside the steps. A step no longer shows its kind and title above the figure; the objects in scope, the assumptions and the clauses alongside are inside one closed line, About this step. And when you select a proof in the editor, Source data shows the statement that the proof proves and keeps the proof closed, so the steps of Lessons 5 to 7 that select a proof go differently, and the route in Lesson 7 through a part of the proof is not offered. Two smaller differences: an object's colour is assigned in order of introduction and can differ from a recorded figure, and the Choices view states each explanation once, in its legend. To follow the lessons exactly, build that revision.

The editor extension package (VSIX) contains only the editor controller. It also needs the matching native engine, browser assets, Lean toolchain and compiled libraries.

Requirements and checked configurations

The declared requirements are Lean 4.28.0, Node.js 22.12 or later, and Git. Editor use also needs VS Code 1.95 or later, the official Lean extension (leanprover.lean4), and a trusted project whose imports have been built. A setup that downloads its own copy of the pinned Mathlib revision can use several GB.

The initial local installation checks used macOS arm64, Node.js 24.18.1, npm 11.16.0 and VS Code 1.138. They do not establish support for every combination of these versions. Linux, WSL, remote hosts, other architectures and the declared minimum Node.js and VS Code versions have not been checked. Native Windows linking is not implemented.

Build from a matching checkout

The local setup guide gives the assembly commands and pinned dependencies for the build it describes, and says what has been checked. Start with its prerequisites.

Assembly installs JavaScript dependencies, prepares the Lean environment and native engine, builds the browser assets, verifies the local setup, and packages the editor controller. Packaging the VSIX alone does not assemble a working installation. The Reference explains Definograph’s other limits.

Use trusted source

The editor has Lean read the whole file again, not only the selected range: it re-elaborates the whole active buffer. Lean commands, macros and elaborators can execute project code; selecting a range does not isolate it from the rest of the file. Build changed imports with the project’s normal tools before refreshing.

Dependency installation uses npm ci --ignore-scripts. This suppresses dependency lifecycle scripts during that installation. The build, setup and packaging commands you run afterwards still execute code. The separate engine process does not provide a security sandbox.

Report a problem

Use the issue tracker. Include the source revision, operating system, tool versions, and the command or editor action that failed.