Setup and release status

Public release status

A complete public distribution has not yet been qualified. There is no installer offered here. The public repository contains project source, but a clone must not be assumed to match the locally checked implementation described in the setup guide.

The 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 requires VS Code 1.95 or later, the official Lean extension (leanprover.lean4), and a trusted project whose imports have been built.

Local checks used macOS arm64, Node.js 24.18.1, npm 11.16.0 and VS Code 1.138. Those checks 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 remain unqualified. Native Windows linking is not implemented.

Build from a matching checkout

The local setup guide gives the assembly commands, pinned dependencies and release qualifications for the implementation it describes. Start with its prerequisites and revision information.

Assembly installs JavaScript dependencies, prepares the Lean environment and native engine, builds the browser assets, verifies the local setup, and packages the controller. Keep these components at the same source revision. Packaging the VSIX alone does not assemble a working reader.

The reference explains the setup requirements alongside the reader's other limits.

Use trusted source

The editor 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.