This is a port of the community fork of Lean 3. This is what the current mathlib runs on while the lean maintainers are busy developing Lean 4.
I have used various versions of this since October 2019 although I had to resort to a number of hacks such as compiling with gcc or disabling multithreading support due to crashes that went away with the futex fixes from earlier in this cycle. cmake installs a number of headers. These are currently unused, since no corresponding library is installed, but it is conceivable that the shared library will come back in future versions, so I did not try to avoid installing them. All tests pass on amd64 and sparc64. Information for inst:lean-3.32.1 Comment: interactive and automated theorem prover Description: Lean is an open source theorem prover and programming language. It aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs. Maintainer: Theo Buehler <[email protected]> WWW: https://leanprover-community.github.io
lean.tgz
Description: application/tar-gz
