Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
Find a file
Cameron Zwarich d2e604f74d
feat: remove the old compiler (#9275)
This PR removes the old compiler written in C++.
2025-07-09 06:00:46 +00:00
.github chore: CI: restore cache in update-stage0 (#9179) 2025-07-03 20:55:14 +00:00
doc chore: update doc/dev/ffi.md after #9088 (#9112) 2025-07-01 01:00:59 +00:00
images
nix
releases_drafts
script chore: improvements to release automation (#9119) 2025-07-01 02:39:10 +00:00
src feat: remove the old compiler (#9275) 2025-07-09 06:00:46 +00:00
stage0 chore: update stage0 2025-07-08 14:35:54 +00:00
tests fix: typos in ISO 8601 formatted datetime (#9235) (#9263) 2025-07-09 05:52:25 +00:00
.gitattributes
.gitignore feat: further release automation (#9092) 2025-06-30 05:44:10 +00:00
.gitpod.Dockerfile
.gitpod.yml
.ignore
CMakeLists.txt chore: compile stage 0 against correct version string (#9085) 2025-06-29 20:52:46 +00:00
CMakePresets.json
CODEOWNERS chore: Update CODEOWNERS (#9232) 2025-07-07 13:11:41 +00:00
CONTRIBUTING.md
flake.lock
flake.nix
lean-toolchain
lean.code-workspace
LICENSE
LICENSES
README.md
RELEASES.md

This is the repository for Lean 4.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.