max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
39951 commits 1 branch 0 tags 5.3 GiB
Find a file
Mac Malone 9eb249e38c
fix: lake: error on executables with duplicate root module names (#13028) 
This PR adds a check that rejects Lake configurations where multiple
executables share the same root module name. Previously, Lake would
silently compile the root module once and link it into all executables,
producing identical binaries regardless of differing `srcDir` settings.

Lake (and Lean) rely on module names being unique within a package.
Rather than attempting to support duplicate module names, Lake now
produces a clear error at configuration load time, for both TOML and
Lean configuration files.

Closes #13013

🤖 Prepared with Claude Code

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
2026-03-23 18:10:10 +00:00
.claude chore: speed up test suite slightly (#12969) 2026-03-20 12:24:32 +00:00
.github chore: CI: bump git cache to 5GB (#13053) 2026-03-23 08:58:35 +00:00
.vscode chore: replace workspace file with .vscode/ settings (#12770) 2026-03-04 01:10:04 +00:00
doc feat: unfold and rewrap instances in inferInstanceAs and deriving 2026-03-22 13:25:46 +01:00
images
releases_drafts chore: remove stale release draft notes (#12518) 2026-02-17 19:56:23 +00:00
script fix: handle lean4-nightly toolchain prefix in release checklist (#12865) 2026-03-23 03:01:58 +00:00
src fix: lake: error on executables with duplicate root module names (#13028) 2026-03-23 18:10:10 +00:00
stage0 chore: update stage0 2026-03-23 15:31:56 +00:00
tests fix: lake: error on executables with duplicate root module names (#13028) 2026-03-23 18:10:10 +00:00
.gitattributes chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
.gitignore chore: replace workspace file with .vscode/ settings (#12770) 2026-03-04 01:10:04 +00:00
.gitpod.Dockerfile chore: add gitpod configuration (#6382) 2024-12-15 21:38:13 +00:00
.gitpod.yml chore: add gitpod configuration (#6382) 2024-12-15 21:38:13 +00:00
.ignore chore: ignore stage0/ (for rg etc.) 2022-03-18 15:28:20 +01:00
CMakeLists.txt chore: make leantar available in stage0 (#12992) 2026-03-19 20:43:43 +00:00
CMakePresets.json chore: fix ci for new test suite (#12704) 2026-02-27 23:25:37 +00:00
CODEOWNERS chore: make @hargoniX code owner of the compiler (#10732) 2025-10-10 04:43:38 +00:00
CONTRIBUTING.md chore: migrate pkg tests (#12889) 2026-03-11 18:55:46 +00:00
flake.lock chore: update to c++20 (#12117) 2026-02-11 01:17:40 +00:00
flake.nix chore: add aarch64-darwin to flake (#12915) 2026-03-18 15:55:34 +00:00
lean-toolchain chore: relative lean-toolchains (#12652) 2026-02-25 10:23:35 +00:00
LICENSE chore: remove LICENSE header that confused GitHub 2021-11-18 09:42:35 +01:00
LICENSES feat: bundle leantar with Lean (#12822) 2026-03-09 20:10:59 +00:00
README.md doc: update URLs that are currently pointing to redirects (#10397) 2025-09-17 15:50:07 +00:00
RELEASES.md chore: updates to release_checklist.md (#7817) 2025-04-04 03:45:36 +00:00

README.md

This is the repository for Lean 4.

About

Installation

See Install Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.