max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update FAQ

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-23 10:19:15 -08:00
parent d5c7f91b83
commit 5b23efc112
1 changed files with 10 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
doc/faq.md
View file

@ -27,39 +27,32 @@ we may be busy, etc. If you really need this new feature or bug fix, we suggest
* Where is the documentation?
The [Lean tutorial](https://leanprover.github.io/theorem_proving_in_lean) is a good introduction to the system.
It may contain a few inconsistencies due to recent changes, but we try to keep it in sync.
The reference manual is work in progress, and we don't know when it will be ready.
The core and math libraries contain many definitions and proofs, they demonstrate how we expect the system to be used.
If the lack of documentation is an issue, then Lean is not a good match for you.
Documentation is not the main priority right now. Recall that Lean is a research project and not a product.
This is the Lean 4 manual. It is working progress, but it will eventually cover the whole language.
A public and very active chat room dedicated to Lean is open on [Zulip](https://leanprover.zulipchat.com).
It is a good place to interact with other Lean users.
You may also join the [Lean user forum](https://groups.google.com/forum/#!forum/lean-user) on Google Groups.
* Should I use Lean to teach a course?
Lean has been used to teach courses on logic, type theory and programming languages at CMU and the University of Washington.
The lecture notes for the CMU course [Logic and Proof](https://leanprover.github.io/logic_and_proof) are available online.
The lecture notes for the CMU course [Logic and Proof](https://leanprover.github.io/logic_and_proof) are available online,
but they are for Lean 3.
If you decide to teach a course using Lean, we suggest you prepare all material before the beginning of the course, and
make sure that Lean attends all your needs. You should not expect we will fix bugs and/or add features needed for your course.
* Are there IDEs for Lean?
Yes, the two main ones are for [Emacs](https://github.com/leanprover/lean-mode) and [VS Code](https://github.com/leanprover/vscode-lean).
The Emacs Lean mode is available via [MELPA](https://melpa.org/). The VS Code Lean extension is available on its marketplace.
We currently have a very simple [Emacs mode](https://github.com/leanprover/lean4/tree/master/lean4-mode) for Lean 4.
Lean 3 supports many IDEs, the two main ones are for [Emacs](https://github.com/leanprover/lean-mode) and [VS Code](https://github.com/leanprover/vscode-lean).
* Is Lean sound? How big is the kernel? Should I trust it?
Lean has a relatively small kernel. The [leanchecker](https://github.com/leanprover/lean/tree/master/src/checker) is a bare-bones version of the Lean kernel.
There are also two independent checkers: [tc](https://github.com/leanprover/tc) and [trepplein](https://github.com/gebner/trepplein).
We have implemented several kernel extensions to improve performance and make sure the system is reasonably responsive for interactive use.
We strongly recommend you frequently check your project without these extensions. The command line option `-t0` disables all of them.
As far as we know, no proof of `false` has ever been accepted by Lean when using `-t0`.
If you are really concerned about soundness, we recommend you often export your project and recheck it using the independent checkers above.
Lean has a relatively small kernel.
Several independent checkers have been implemented for Lean 3. Two of them are
[tc](https://github.com/leanprover/tc) and [trepplein](https://github.com/gebner/trepplein).
We expect similar independent checkers will be built for Lean 4.
* Should I open a new issue?
We use [github](https://github.com/leanprover/lean/issues) to track bugs and new features.
We use [github](https://github.com/leanprover/lean4/issues) to track bugs and new features.
Bug reports are always welcome, but nitpicking issues are not (e.g., the error message is confusing).
RFC issues are created by developers only.