lacker / lean Goto Github PK

License	Continuous integration	Chat

• Important: This is Lean 3.21.0c, a fork of Lean 3 maintained and updated by the Lean community. The last official release of Lean 3.x was Lean 3.4.2, which can be found here. The Lean developers are currently developing Lean 4.
• Lean Homepage
• Lean Prover Community Homepage
• Theorem Proving in Lean
• Change Log
• Lean 3.4.2 FAQ
• For HoTT mode, please use Lean2.

The recommended way to install Lean is following these instructions under Regular install.

If you just want to modify the core library (not the C++ source), you can run (in your local lean/ directory)

git checkout v3.xx.x
git checkout -b my-branch-name
elan override set leanprover-community-lean-3.xx.x

You can now build the core library with lean --make library or open any Lean file is VSCode / Emacs and it will use the version of Lean you specified. You might have to restart Lean (in VScode: ctrl+shift+P Lean: Restart). Warning: editor features, like Go to Definition will not behave correctly with this setup. For the best experience, build Lean from source.

Stable binary releases of Lean are available on the release page. Nightly binary releases are available on the nightly release page. For building Lean from source, see the build instructions.

• Building Doxygen Documentation: doxygen src/Doxyfile
• Coding Style
• Library Style Conventions
• Git Commit Conventions
• Syntax Highlight Lean Code in LaTeX
• Exporting, and reference type-checkers