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.
31525 commits 1 branch 0 tags 5.3 GiB
Find a file
Siddharth a436c225d8
chore: disable lake 116 test (#2358) 
The test is flaky due to the presence of a fixed 'sleep()'.

The LLVM backend has introduced a performance
regression in Lake which causes this test to fail, as the
current sleep duration of 3s is insufficient.
Further investigation into the performance regression is pending.

We decided to disable the `leanlaketest_116` entirely on account
of the test being flaky by construction
(https://github.com/leanprover/lean4/pull/2358#issuecomment-1655371232).
2023-07-29 09:40:18 +00:00
.github fix: do not use GMP on ARM Linux 2023-07-13 09:35:00 +02:00
.vscode doc: fix some syntax and link in the docs, and more 2021-10-10 11:36:43 +02:00
doc chore: Nix bump to LLVM 15 2023-07-28 10:56:54 +02:00
images
nix chore: Nix bump to LLVM 15 2023-07-28 10:56:54 +02:00
script chore: remove unused macOS dependencies 2023-07-26 15:36:36 +02:00
src chore: disable lake 116 test (#2358) 2023-07-29 09:40:18 +00:00
stage0 chore: update stage0 2023-07-25 11:03:16 +02:00
tests fix: symmetry in orelse antiquotation parsing 2023-07-28 08:36:33 -07:00
.gitattributes chore: ensure consistent (Unix) encoding for source files 2023-03-10 16:27:56 +01:00
.gitignore chore: avoid xargs in update-stage0 2022-11-20 10:22:20 -08:00
.ignore chore: ignore stage0/ (for rg etc.) 2022-03-18 15:28:20 +01:00
CMakeLists.txt fix: forward USE_GMP to stage 0 2021-12-02 15:52:48 +01:00
CONTRIBUTING.md chore: update CONTRIBUTING.md 2023-02-01 12:07:15 -08:00
default.nix
flake.lock chore: Nix bump to LLVM 15 2023-07-28 10:56:54 +02:00
flake.nix chore: Nix: use strings instead of URL literals (#2172) 2023-03-28 10:10:24 +02:00
LICENSE chore: remove LICENSE header that confused GitHub 2021-11-18 09:42:35 +01:00
LICENSES chore: add GMP license for now 2021-11-18 09:42:35 +01:00
README.md doc: clarify current release process 2023-06-30 10:30:37 -07:00
RELEASES.md doc: fix typos (#2287) 2023-06-25 20:30:33 +02:00
shell.nix chore: Nix bump to LLVM 15 2023-07-28 10:56:54 +02:00

README.md

This is the repository for Lean 4, which is being actively developed and published as nightly releases. Stable point releases are planned for a later date after establishing a robust release process.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.