Tools explained

Stream: general

[Patrick Massot]

With all the recent messages about weird setups of confused users, I finally had at shot at writing the tool chain explanation I've been meant to write forever. I got a bit tired at the end, but I hope the main points are there. I put a draft at https://gist.github.com/PatrickMassot/68109ad8143dcdced860f1aed3495fc9. Comments are welcome. I think even moderately experienced users could learn a thing or two, or at least enjoy the global view. If some people like it I'll propose some version of this in the community documentation.

[Kevin Buzzard]

"Now check lean --path from outside or inside the folder containing leanpkg.path to see the difference." -- if they still have LEAN_PATH set then they won't see a difference :-)

[Patrick Massot]

I explained how to set it only when launching Lean. I didn't write to set it globally.

[Patrick Massot]

That's what LEAN_PATH=path_to_our_lean_install_folder/lib/lean/library/:path_to_folder_containing_test lean test2.lean is doing

[Johan Commelin]

Thanks! I fixed some typos: https://gist.github.com/jcommelin/50651ec7932bf8f641ca31f60f6a6465

[Johan Commelin]

I thought you could PR from a fork of a gist to the original... but I can't find the option now

[Koundinya Vajjha]

This is great. Thanks a lot for writing this @Patrick Massot !

[Patrick Massot]

Ok, I created https://github.com/leanprover-community/mathlib/pull/2337. Feel free to contribute!