Being more inviting for research mathematicians to use Lean

Stream: general

[Alex Kontorovich]

We were discussing offline how to make Lean more accessible to research mathematicians. I'm told that Lean+Mathlib can now be downloaded with one click as a single *.dmg file (for Mac) that just needs to be opened and it'll install everything -- is that right? If so, I couldn't find it.

As a test, I went to the main site, navigated easily to the install instructions (https://leanprover-community.github.io/install/macos.html), and I see this:
image.png
First there's a big warning that you have to trust us and that we promise we won't do anything nefarious to your system. (Only people who do nefarious things say that!...) Then there are scary unfamiliar words like elan and sudo, and you have to open a terminal; I think this is already where you'll lose the vast majority of mathematicians who want to try it on their own (even ones who have already successfully played something like the Natural Numbers Game online). Yes, there are lots of suggestions along the way for anyone to "just" come to zulip and ask for help; but I think people underestimate just how frightening that proposition is, even for established researchers... Please let me know if I'm wrong...?

[Jireh Loreaux]

I think we should probably now just link directly to https://lean-lang.org/lean4/doc/quickstart.html, and then add a comment about how to get a project which depends on Mathlib (which is also available just by clicking VS Code buttons at this point).

[Jireh Loreaux]

People who prefer emacs or vim might be disappointed at installing VS Code, but I also suspect such users are more likely to go hunting fore more information.

[Adam Topaz]

FWIW, I think to make lean more accessible we as a community should spend more time making the use of various "in-browser" tools (like github code spaces, gitpod, etc.) as smooth as possible. No trust is needed (except for, say, making a github account with an email address). I think github codespaces is actually quite nice to use, but the workflow of making pull requests, git branches, etc., can overwhelm a lot of people.

[Adam Topaz]

It's crazy, but I think many students (and maybe even postdocs and professors) don't even install latex anymore, and just end up using overleaf.

[Adam Topaz]

Jireh Loreaux said:

People who prefer emacs or vim might be disappointed at installing VS Code, but I also suspect such users are more likely to go hunting fore more information.

I think quitting (n)vim and/or emacs is at about the same level of difficulty as installing elan. So I'm not too concerned about this.

[Mario Carneiro]

do you mean from an installation complexity standpoint? Asking someone to switch to a new editor interaction mode can be very difficult even if there is no installation difficulty at all

[Adam Topaz]

Well, what I mean is that some level of technical ability/knowledge is required for using vim/emacs, and I expect that such people are comfortable with words like "sudo" and reading docs that mention the command line. So I don't think such people are what Alex is talking about in the original message.

[Adam Topaz]

That's also how I understood Jireh's comment about vim/emacs users.

[Adam Topaz]

Of course I agree with you (Mario) that it's not easy for someone who has been using vim for 30 years to all of a sudden switch to VScode. But I think the solution to that issue is for the nvim and emacs packages to get more dev attention, and for us to update the editor section in the installation pages such as this one: https://leanprover-community.github.io/install/macos_details.html

[Matthew Ballard]

All my recent collaborations confirm: overleaf is the dominant market force force any type of team latex use

[Matthew Ballard]

I think the technology exists for a full VS Code experience via the browser these days beyond Codespaces and Gitpod.

[Patrick Massot]

Matthew Ballard said:

All my recent collaborations confirm: overleaf is the dominant market force force any type of team latex use

The world has gone crazy…

[Ruben Van de Velde]

How so?

[Frédéric Dupuis]

Patrick Massot said:

The world has gone crazy…

We're even starting to see this in CS departments, I don't even want to think about how bad it is elsewhere!

[Mario Carneiro]

I don't think there is anything weird about not wanting to install a large piece of software with many moving parts and an infinite number of installation failure cases. I'm currently working on a group paper and some of our members still can't get the paper to build properly locally

[Mario Carneiro]

Lean is no different in this respect, although my impression is that we have better tooling for avoiding the installation edge cases because we bundle more

[Miguel Marco]

Matthew Ballard said:

I think the technology exists for a full VS Code experience via the browser these days beyond Codespaces and Gitpod.

Running Lean on a nontrivial project can be quite CPU intensive. That means that, a cloud service that provides it will face a significant electricity bill.

And about running Lean in the browser instead of the server... loading the full mathlib sounds very big for that kind of approach.

[Ruben Van de Velde]

You know that this already exists?

[Miguel Marco]

You mean the in-browser option or the cloud one?

[Yaël Dillies]

Both?

[Shreyas Srinivas]

What's the in-browser option?

[Yaël Dillies]

gitpod.io

[Shreyas Srinivas]

Afaik that's cloud

[Shreyas Srinivas]

They don't run lean inside the user's browser

[Yaël Dillies]

Ah, I thought in-cloud not-in-browser would mean something like a remote server you SSH into

[Shreyas Srinivas]

In-browser would be a wasm port of lean served along with an editor. This could then be combined with the current extension by making it work on vscode web. IIRC even live.lean-lang.org runs lean on the server, unless this changed recently

[Eric Wieser]

Mario Carneiro said:

I don't think there is anything weird about not wanting to install a large piece of software with many moving parts and an infinite number of installation failure cases.

Especially if you already installed some other large software, and the two disagree on how the parts should move. Sure, docker containers etc solve this problem too, but it's much easier to let a cloud provider deal with the containers than to manage them yourself; and your local power usage is hopefully lower as a result too!

[Eric Wieser]

I ended up ditching overleaf for my thesis due to performance issues, but switched to gitpod rather than a local install so that I could be sure that there was no risk of a laptop failure leaving me facing a reinstallation that inevitably doesn't behave the same way as the original.

[Shreyas Srinivas]

overleaf is super expensive and their compile limits are very limiting. I can't even compile stuff that was fine 3 years ago, so I am guessing the compile limits are worse now.

[Jon Eugster]

Shreyas Srinivas said:

IIRC even live.lean-lang.org runs lean on the server, unless this changed recently

That's true.

There is in theory wasm for lean 4, @Alexander Bentkamp implemented that and did run some code in browser at some point. But no full mathlib (if any imports at all?).

[Julian Berman]

Yaël Dillies said:

Ah, I thought in-cloud not-in-browser would mean something like a remote server you SSH into

(Gitpod thankfully supports this just fine :)

[Shreyas Srinivas]

@Alex Kontorovich : researchers who want to try out lean before doing something serious could use live.lean-lang.org
I often use it as a scratchpad these days. The installation process from inside the vscode extension also works smoothly for math purposes.

[Mario Carneiro]

lean is a total resource hog these days, wasm is impractical. I consider this a very unfortunate state of affairs, and a significant factor in why the FRO has gone 100% mathlib-free

[Shreyas Srinivas]

Can't we actually create a lean app for the macOS app store whose job is to install everything, show a project view and open a chosen project in vscode?

[Shreyas Srinivas]

will they accept such an app?

[Mario Carneiro]

Apple has a bunch of licensing restrictions and signing requirements on things in the app store, I wouldn't be surprised if it's technically infeasible

[Miguel Marco]

What about the trylean bundle approach? Woukd that work on MacOS or would it also be blocked by the security features of the system?

[Shreyas Srinivas]

Hmm.. then a dmg is pointless. macOS requires extra steps to install DMGs from the internet. At that point one is better off installing vscode and following the vscode lean install process. similar number of steps.

[Kim Morrison]

Jireh Loreaux said:

I think we should probably now just link directly to https://lean-lang.org/lean4/doc/quickstart.html, and then add a comment about how to get a project which depends on Mathlib (which is also available just by clicking VS Code buttons at this point).

Is someone taking this on? This seems like the low-hanging fruit here!

[Patrick Massot]

We were waiting for Marc to tell us this was ready. But I guess everybody forget to follow up. This only things that worries me a bit is that this will lead people to think those menus are reliable and they will be disappointed when trying to update projects.

[Jireh Loreaux]

Should I completely remove the "detailed" guides, or should we leave them but with the link to quickstart displayed first and most prominently?

[Johan Commelin]

I would keep them around. But they can be on a separate page.

[Johan Commelin]

Like with the linux version

[Florent Schaffhauser]

FWIW, I still remember getting started on installing Lean and, as a beginner and research mathematician, finding the information on https://leanprover-community.github.io/install/macos.html, and leanprover-community.github.io in general, absolutely invaluable. So, if you are interested in an outsider's opinion on that, I would kindly ask you to keep that info somewhere :thank_you:

[Marc Huisinga]

Patrick Massot said:

We were waiting for Marc to tell us this was ready. But I guess everybody forget to follow up. This only things that worries me a bit is that this will lead people to think those menus are reliable and they will be disappointed when trying to update projects.

To be clear, my point was that we should keep the detailed guide in leanprover-community around because it's valuable information for anyone who needs the details instead of simply deleting it. Linking to the quickstart guide and keeping the leanprover-community guide around as a more detailed and more manual guide would be perfectly fine with me!

[llllvvuu]

Running Lean on a nontrivial project can be quite CPU intensive. That means that, a cloud service that provides it will face a significant electricity bill.

Gitpod's pricing is not bad actually, taking into account 50 hours free per month (the equivalent Codespaces offering has the same hourly rate plus 30 free hours, I guess you could double-dip). They are targeting serious developers to use this full-time, so I guess it has to be somewhat viable from cost and latency POV.

[Yaël Dillies]

Also note that if you're contributing to mathlib you can send them an email to the effect of "I'm contributing to open source software" and they will raise your amount of free hours per month to 250

[Yaël Dillies]

(Eric Wieser and I do manage to use 250h/month sometimes)

[Jireh Loreaux]

https://github.com/leanprover-community/leanprover-community.github.io/pull/453