Lean toolchain doc

Stream: lean4

[Patrick Massot]

Back in the old days of Lean 3, we often had people who didn't want to use the recommended setup, complained about having to install some python-based supporting tools, or simply were confused by how all those pieces fitted together. I wrote https://leanprover-community.github.io/toolchain.html for those people. We could simply get rid of this webpage, but I think it would be nice to have a Lean 4 version. However this would require very heavy editing. @Mac Malone and @Wojciech Nawrocki, you know a lot more about the project infrastructure and Lean editor protocol. Would you be interested in working on this update?

[Mac Malone]

@Patrick Massot I am happy to answer any questions and review any new drafts. :grinning_face_with_smiling_eyes: From a design standpoint, though, I am conscious of the overlap with the Lean 4 manual. If a detailed overview of the Lean 4 toolchain is developed, it might be worth discussing where it would be best located (and if the other locations should duplicate some of the material or link to it).

[Patrick Massot]

That's a fair point. What happened in the Lean 3 is that the full toolchain (not in the elan sense) included mathlib-only stuff. As far as I understand, this is still true as long as lake exe cache get is a mathlib thing and not a purely lake thing.

[Mario Carneiro]

@Mac Malone I think it is worth the duplication, because there will always be mathlib-only stuff and the lean 4 manual tends not to mention mathlib that much, which makes it not a good place to survey the whole zoo of tools