Skip to content

installation.md

Latest commit

 

History

History
31 lines (20 loc) · 975 Bytes

installation.md

File metadata and controls

31 lines (20 loc) · 975 Bytes

Installation

Lean 4

Install Elan and a compatible Lean toolchain. This repository pins Lean in the lean-toolchain file at the repo root (for example leanprover/lean4:v4.21.0).

git clone https://github.com/SentinelOps-CI/lean-toolchain.git
cd lean-toolchain
lake build

The first lake build downloads mathlib and other dependencies; expect a long compile on a cold cache.

Rust (optional)

Required if you work on the generated crate or run parity tests:

  1. Install Rust (stable).
  2. After Lean changes to the extractor or templates, run lake exe extract, then cargo test (and cargo clippy --all-targets -- -D warnings if you touch Rust) inside rust/.

Documentation tools (optional)

To build the MkDocs site from the same machine:

pip install mkdocs-material
mkdocs build -f docs/mkdocs.yml

See Documentation home for what the pages cover.