Links to Resources for Help

Stream: lean4

[Jonathan Crall]

I'd like to suggest a change to the lean4 README, and the docs for creating an issue led me here.

I'm having trouble finding resources for places I can ask lean4 questions. There is a lot of good stuff in terms of documentation on the README, but that can only go so far. For example, I only learned about elan after a long time of searching. A lot of the resources online are for lean3 and that gets confusing. This seems to be a fairly active discussion page where you can ask questions, so maybe it makes sense to link to this page on the README? (If it's there then I missed it).

Also if there are other places on could seek help with using lean4, a list of places like that would be a helpful addition to the top-level docs.

[Mario Carneiro]

This is definitely the place to ask questions about lean 4

[Mario Carneiro]

you can also ask questions on the proof assistant SE https://proofassistants.stackexchange.com/ , especially if your question applies to multiple proof assistants

[Mario Carneiro]

I am surprised that elan was hard to spot, it should be in the getting started page

[Mario Carneiro]

there is some indirect discussion of elan on step 3 of the quickstart

[Mario Carneiro]

following those instructions will install elan, and you don't normally interact with it directly otherwise

[Mario Carneiro]

the fact that a lot of lean 3 documentation is out there is a problem we are aware of; it is unfortunately quite a lot of effort to make comparable lean 4 documentation (and get it to show up in searches) but it's getting done slowly

[Mario Carneiro]

I agree that the zulip instance should be more prominently shown on the readme; it is at least as important as books like FPIL for getting users situated

[Jonathan Crall]

I'm really a vim+terminal kind of guy, so the vscode instructions are hard for me to follow. The only reason I'm using vscode is because the interactive integration with lean seems very nice, but the magic "install plugin" button is less than helpful when it comes to building understanding. When I try to run new software I've never used, I'm looking for executables and PATH modifications. The example here: https://gist.github.com/jcommelin/1d45a0ea7a84a87db8a28a12e93cac32 is what cued me into elan. The main reason I went looking for it was because I was having a very hard time getting any new lean files to recognize mathlib as something that was importable. This is the other page that helped me out: https://leanprover-community.github.io/install/project.html but there doesn't seem to be singular resource that brings you from zero to: you can write code in this file, reference external libraries, and execute your code like this. Something of that ilk might be very helpful to newcomers like me.

EDIT: I should mention that the quickstart did get me to the point where I could use barebones lean very easilly. It might be good to add a section for "if you want to use mathlib" in addition to if you want to contribute.

[Mario Carneiro]

note that working from an old gist is pretty fraught

[Mario Carneiro]

I see references to 2018 in there, things have changed significantly since then

[Mario Carneiro]

the leanprover-community get started docs here go into a reasonable level of detail for folks who like to use the terminal

[Mario Carneiro]

if you want to use mathlib that's a good place to start

[Mario Carneiro]

other official lean sources mention mathlib as a bit of an afterthought because they are trying to be more broadly applicable

[Alex J. Best]

I think the page https://lean-lang.org/download/ could be improved though. I've certainly seen competent people I've spoken about lean to at workshops speed through the "google name of software > click on first link > click download > click binaries" cycle without reading the "You will usually want to follow the official instructions instead of downloading these releases directly." part at all, and then wondering why nothing works because every step seemed reasonable.

[Mario Carneiro]

I think rust does a good job of steering people looking for downloads to rustup.rs or https://www.rust-lang.org/tools/install

[Mario Carneiro]

I'm pretty sure we want to do the same kind of thing

[Mario Carneiro]

the install page there in particular is well laid out, it's focused on "what do people coming here want" rather than "what do we have"

[Mario Carneiro]

labelling something as "(recommended)" is good for the speedrunners

[James Gallicchio]

maybe it's a good idea to have a topic pinned somewhere for keeping track of old/misleading documentation, so that we can find someone who can take it down or link to the right place :)