lean, elan, leanpkg, leanproject -- documentation?

Stream: new members

[Jasmin Blanchette]

I'm writing this to "new members" because the question is very basic: Is there anywhere an overview of the Lean tools (lean, elan, leanpkg, leanproject), what their raison d'etre is, what they do, what the main concepts behind them is, etc.? Because the truth is, I have no clue. I know how to install Lean but not how to maintain it. leanpkg apparently deals with packages; is that lean, mathlib, and VSCode extension? Are these the three packages? Where is this explained?

Yesterday, @Jannis Limperg gave me access to a branch of a project we work together. He had changed the Lean version in "leanpkg.toml". My VSCode started running out of memory, so I thought: Probably I need to recompile mathlib. How do I do that? Jannis told me:

lean --make file.lean to compile file.lean and its dependencies. You can also go into _target/deps/mathlib and use leanproject get-cache

(Turns out I didn't have leanproject.) How does one, as a novice or as somebody who's been using Lean for 1.5 years and who's still clueless, come up with these commands? I would gladly read the docs, but where are they? And how come this issue (apparently?) is not affecting lots of other novices? I just don't get it. Do people just hang out on Zulip until they just "get" these things?

[Kevin Buzzard]

This has all gone through several iterations.

[Jasmin Blanchette]

For sure. But I used to work as doc manager for several years, and then the docs also went through several iterations.

[Kevin Buzzard]

The short story is that Patrick Massot wrote leanproject, only a few months ago, which was supposed to be a one size fits all tool for doing everything which most users want to do.

[Jasmin Blanchette]

I would already be quite happy with a one para description of each tool.

[Kevin Buzzard]

That's just coming :-)

[Jasmin Blanchette]

Very good. Then I consider my question answered. :)

[Jasmin Blanchette]

And I'll keep bugging my colleagues whenever I have issues until then.

[Kevin Buzzard]

https://leanprover-community.github.io/toolchain.html

[Jasmin Blanchette]

Wow.

[Kevin Buzzard]

https://github.com/leanprover-community/mathlib-tools/blob/master/README.md

[Jasmin Blanchette]

Google didn't find it, sadly, when I looked for recompiling mathlib. It pointed me to your installation notes.

[Kevin Buzzard]

Can you tell me exactly what you mean by my notes?

[Kevin Buzzard]

search is a big problem. Searching for Lean sends you to the MS pages which are very out of date.

[Jasmin Blanchette]

I'll try to find "your notes" again.

[Kevin Buzzard]

The community, Patrick and Rob and others, have put in a huge amount of effort to make a detailed community website with really thorough explanations of a lot of things: https://leanprover-community.github.io/

[Jasmin Blanchette]

Those notes:

https://xenaproject.wordpress.com/2017/12/02/how-to-install-mathlib-and-keep-it-up-to-date/

Regardless, I could see this was not what I was looking for.

[Jasmin Blanchette]

This is really great. I'll study the toolchain page. And the rest of the site. It's exactly what I was looking for.

[Kevin Buzzard]

Patrick has done an extremely thorough job, because although many mathematician users just want to have "leanproject up", many CS users want to know what is going on. He has catered for both.

[Jasmin Blanchette]

I just can't seem to find my way from the front page to toolchain, though.

[Jasmin Blanchette]

If I e.g. click on "Working on Lean projects", then I see "leanproject", I click that, and then I end up staring at a github directory.

[Kevin Buzzard]

The toolchain link is on the install page.

[Jasmin Blanchette]

I see. Thanks. It's really been a big source of frustration and anxiety for me. I guess you're hoping users won't need this? This might be true, but in my experience they will...

[Kevin Buzzard]

I'm absolutely hoping users won't need this if they didn't have a previous Lean installation of any kind.

[Jasmin Blanchette]

My next question then is: How can I completely eradicate Lean from my machine, so that I can become one of these happy users? ;)

[Kevin Buzzard]

What happens if you just follow the installation instructions for your OS? At precisely which point does something not go to plan?

[Patrick Massot]

Jasmin, eradicating Lean should be pretty east, you can simply ask your system where it finds Lean.

[Patrick Massot]

Also, PRs to https://github.com/leanprover-community/leanprover-community.github.io are very welcome if you have ideas about links that should be added.

[Jasmin Blanchette]

But surely there's a bunch of .elan/* etc. files which I should remove, otherwise there's no point, right?

[Jasmin Blanchette]

Kevin, my problem scenario was described in my first message, with Lean running out of memory while rebuilding mathlib in VSCode. That's where things started to derail.

[Jasmin Blanchette]

Which in turn happened because somebody changed some Lean and mathlib versions in a repository's leanpkg.toml file.

[Jasmin Blanchette]

I'd expect such things happen all the time to people whenever they update leanpkg.toml. They need to do some stuff on the command line; otherwise, they'll have to wait in VS Code and maybe, like me, get weird memory-related errors.

[Kevin Buzzard]

I mean what happens if you follow the installation instructions for getting leanproject. Nothing to do with running Lean on a file.

[Kevin Buzzard]

leanproject up should solve your problems

[Kevin Buzzard]

or in your case leanproject get-cache

[Kevin Buzzard]

Yes, leanproject up changes your toml (and recompiles mathlib for you). If someone else changes the toml in a shared project then you can either do git pull and then something like leanproject get-mathlib-cache or something, or you can just follow the xkcd advice, delete the project completely and re-install it with leanproject get <path to project>

[Jasmin Blanchette]

I haven't tried to install leanproject yet (since I didn't know what problem it was supposed to solve for me).

[Jasmin Blanchette]

I'll give what you write a try once I'm done with all my Skype/etc. calls.

[Jasmin Blanchette]

Thanks for the help!

[Rob Lewis]

Jasmin Blanchette said:

I haven't tried to install leanproject yet (since I didn't know what problem it was supposed to solve for me).

Your grant money is (was) paying for it ;)

[Jasmin Blanchette]

"Lots of wonderful things on the community web site, all hidden under two layers of links." -- Anonymous (Gabriel E.)

[Jasmin Blanchette]

"I recognize a hard-to-navigate web site when I see one." -- Anonymous

[Jasmin Blanchette]

"There's a massive amount of interesting content." -- A

[Patrick Massot]

I think users that installed Lean a long time ago but didn't keep up to date are a difficult target for us. It's much easier to deal with real beginners. But again you can very easily PR changes to the website.

[Kevin Buzzard]

@Jasmin Blanchette I think that if someone else changes the toml of a project you are working on, if this project has mathlib as a dependency (and no other dependencies), and if you have leanproject, you can git pull and then (in the root directory) rm -rf _target and then leanproject get-mathlib-cache. I just tried this in exactly your situation and it seems to work fine.

[Kevin Buzzard]

@Patrick Massot what I've said is not correct -- if you remove _target then get-mathlib-cache gives you Lean and olean files, but it doesn't make mathlib into a git repo (and this was an issue for me because my script for compiling the real number game needs the fact that mathlib is a git repo apparently). I genuinely don't know what the workflow is supposed to be if someone else working on a joint repo changes leanpkg.toml.

[Jannis Limperg]

I'm afraid most leanproject commands won't work for you, Jasmin, because the root directory of our Lean project is not also the root directory of a Git repository (see this issue). But cd _target/deps/mathlib; leanproject get-cache works.

[Jannis Limperg]

So overall, what I do after an update to leanpkg.toml is

$ leanpkg configure
[this checks out the correct mathlib commit in _target/deps/mathlib]
$ cd _target/deps/mathlib
$ leanproject get-cache [or leanpkg build if there's no cache available]

[Patrick Massot]

The answer hasn't change: if you decide to break all rules then you're on your own, but you can still submit a PR to the tooling, as long as it doesn't break stuff for people who follow the instructions.

[Jannis Limperg]

Yes of course, no complaining intended. ;)

[Patrick Massot]

Note that I'm not complaining either, and I'm serious when I say that PRs are welcome.

[Jiekai]

One thing puzzles me is about elan.
Running which lean gives me ~/.elan/bin/lean, which is not the lean executable from the release. Why?

[Johan Commelin]

Magic

[Johan Commelin]

This ~/.elan/bin/lean figures out which lean you really want, and then executes that.

[Dima Pasechnik]

the procedure to install leanproject is not really foolproof. 1st of all, it's not normal to call sudo pip, unless you are willing to place 100% trust into what you're going to install, and it has potential to nuke your precious system Python. One normally would do stuff in venv, or pip install ... --user, which installs things into your $HOME. Anyway, pip does not adjust your PATH, and so one possibly needs to pay attention to pip's warnings, telling you to adjust PATH`.

[Patrick Massot]

The idea is that if you know about venv you don't need any instruction here.

[Patrick Massot]

And if you don't then you won't nuke your system Python (hopefully).

[Kevin Buzzard]

Right. The target audience here are mathematicians who are terrified of the command line.

[Dima Pasechnik]

Patrick Massot said:

And if you don't then you won't nuke your system Python (hopefully).

this assumes that the provider of leanproject never screws up. :-)

[Dima Pasechnik]

Kevin Buzzard said:

Right. The target audience here are mathematicians who are terrified of the command line.

You also assume that everyone has /usr/local/bin in PATH, which need not be the case, and in this case the scripts installed bysudo pip3 install mathlibtools will be hidden (from the commandlinefrightened user :-)).

[Patrick Massot]

Of course we know this is not perfect. Any improvement is welcome.

[Kevin Buzzard]

In the rest of the docs we try and encourage the reader to download a command line which works.

[Alex J. Best]

Whats wrong (if anything) with pip3 install --user mathlibtools instead? (I think I've subconsciously been using that all along, but I'm not sure)

[Dima Pasechnik]

Alex J. Best said:

Whats wrong (if anything) with pip3 install --user mathlibtools instead? (I think I've subconsciously been using that all along, but I'm not sure)

indeed, this is better than using sudo - some people are on shared computers, you know. I've made
https://github.com/leanprover-community/leanprover-community.github.io/pull/74

[Patrick Massot]

Insulting us won't improve things.

[Dima Pasechnik]

Patrick Massot said:

Insulting us won't improve things.

excuse me? how am i insulting anyone here?

[Dima Pasechnik]

a student might want to work on the project from a shared computer in a lab. She won't have the rights to do sudo?

[Dima Pasechnik]

jeez...

[Dima Pasechnik]

where is an insult? that I assumed I know a thing or two more about Python than you guys? yes I do. if you find it insulting I'll leave.

[Jalex Stark]

i think some of us are appreciative to hear about better solutions

[Jalex Stark]

so far I think you mostly have pointed to decisions that leanproject maintainers made and implied that they are obviously bad

[Dima Pasechnik]

Jalex Stark said:

i think some of us are appreciative to hear about better solutions

it is well-known that it's better not to use sudo if you can aviod it. besides, there are settings you can't do sudo. Say, you came to Oberwolfach and your laptop died, so you use a shared Linux machine, no sudo...

[Jalex Stark]

I think the main goal of these instructions is to maximize the probability that the user gets a working install without quitting

[Dima Pasechnik]

I've spent some time writing a PR that was closed as insulting. I want to hear an apology for this, to begin with...

[Jalex Stark]

when you say it is well-known that it is "better" not to use sudo, your notion of better may not be aligned with the goals of this project, and in fact it may require a nontrivial argument to see whether it is better or not

[Dima Pasechnik]

Why was my attempt to contribute something deemed an insult? This is just crazy.

[Jalex Stark]

I think the thing in your PR that causes me not to take it seriously is "(look, no sudo)". Who is the audience of that remark?

[Jalex Stark]

it's insulting that you seem very certain your change furthers our goals, notice that we don't have the same level of certainty, and don't seem to make any epistemic update

[Dima Pasechnik]

I am open to criticism, I can edit things if they can be improved. I can edit this joke out, sure.

[Jalex Stark]

I think the development cycle we usually do is have a zulip thread to figure out whether a change is desired before opening a PR

[Jalex Stark]

so could you explain what kinds of trouble we can cause for people by instructing them to use sudo? we don't seem to have any empirical evidence of such a problem

[Dima Pasechnik]

There was a remark "Any improvement is welcome". So I made a PR. Whcih was closed as "insulting", by the same who said "welcome". This is gaslighting of worst kind.

[Alex J. Best]

I think without the "(look, no sudo)" is fine, but it should also be applied to the linux.md macos.md right? It seems windows is alright as it is.

[Dima Pasechnik]

Jalex Stark said:

so could you explain what kinds of trouble we can cause for people by instructing them to use sudo? we don't seem to have any empirical evidence of such a problem

if a rogue contribution gets in then a lot of damage may be done by installing your project with sudo.

[Jalex Stark]

I see. so this is a security issue of the sort "if someone wants to infect a bunch of mathematician's computers with malware, they only have to pass the review process for elan"?

[Dima Pasechnik]

well, just someone with commit rights gets angry... this is what happens now and then.

[Jalex Stark]

this seems like the sort of thing that sufficiently small communities should ignore and sufficiently large communities should pay attention to.

[Dima Pasechnik]

well, you turn some people away, just because you ask them to install things with sudo. They might not trust you 100%. Neither they should.

[Alex J. Best]

I think the issue of shared machines where people do not have sudo is also quite relevant, its pretty common in academic departments after all.

[Dima Pasechnik]

Many departments issue people laptops without sudo rights, too.

[Dima Pasechnik]

bad things happen, projects, big or small, get hacked, binary blobs infused with malware, etc. GitHub might get hacked.

[Jalex Stark]

if we hope to improve our advice, we should aim to make the new advice about as foolproof as the old advice, (so that we don't lose people in the other direction, where the instructions were too hard) and as easy to follow as copy pasting terminal commands and answering yes/no questions about their outputs

[Dima Pasechnik]

the present advice is not foolproof, not only as sudo rights might be absent, but also as it assumes that /usr/local/bin is in PATH. Which might or might not be the case.

[Scott Morrison]

We do want to make sure we keep the instructions as simple as possible. Once we've sorted out the "preferred suggestion", we should write the install instructions so as to present just that one suggestion, and then either on a second page or at the bottom of the page we can have the "advanced usage" notes, e.g. explaining how to check and fix your PATH, or to use whichever of sudo and --user isn't the preferred suggestion.

[Johan Commelin]

Can someone tell me what is the downside of --user?
I've been using it all the time (because I don't care to look up my sudo password, yes, it's long). As far as I can see it doesn't make anything any more complicated.

[Johan Commelin]

I sense a lot of pushback to a change that is (as far as I can see) very innocent, and arguably an improvement.

[Johan Commelin]

Sure the (look, no sudo) might better be left out. But come on guys. Don't overreact if someone is making a first PR.

[Markus Himmel]

I'd like to suggest yet another way of installing leanproject:

python3 -m pip install --user pipx
python3 -m pipx ensurepath
pipx install mathlibtools

pipx is essentially a wrapper around pip for installing end-user applications. The second command automatically adds the correct directories to the user's PATH. The third command installs leanproject (no sudo required) and it also does all the venv isolation magic. This way of installing should also protect against accidentally using Python 2.

[Scott Morrison]

Wheels within wheels! :-)

[Dima Pasechnik]

By the way, I don't see why the whole process of installing elan+mathlibtools is not wrapped into one command.

[Johan Commelin]

It is

[Dima Pasechnik]

Markus Himmel said:

I'd like to suggest yet another way of installing leanproject:

python3 -m pip install --user pipx
python3 -m pipx ensurepath
pipx install mathlibtools

pipx is essentially a wrapper around pip for installing end-user applications. The second command automatically adds the correct directories to the user's PATH. The third command installs leanproject (no sudo required) and it also does all the venv isolation magic. This way of installing should also protect against accidentally using Python 2.

neat, I didn't know about pipx!

[Johan Commelin]

@Dima Pasechnik See the one-liner on https://leanprover-community.github.io/install/debian.html

[Dima Pasechnik]

Johan Commelin said:

Dima Pasechnik See the one-liner on https://leanprover-community.github.io/install/debian.html

ah, OK.

[Dima Pasechnik]

Johan Commelin said:

Sure the (look, no sudo) might better be left out. But come on guys. Don't overreact if someone is making a first PR.

I probably did a hundred PRs on GitHub (107 closed and 12 open currently, as GH dashbord tells me), but this is the 1st one that turned into a PR disaster. One way or another, I'd really suggest someone removing/hiding that We're not interested in merging insults to the community. before it's all over social media...

[Sebastien Gouezel]

I agree. I have hidden Patrick's message (but if he really wants to he can definitely unhide it!).

[Sebastien Gouezel]

Do you think you can also amend your PR to remove the sudo joke, and then maybe we can forget about all this and start afresh? I am really happy to have you here, and I think your PR is an improvement on what we currently have. But mathlibtools is Patrick's baby, so he will have the final word on this.

[Dima Pasechnik]

Sorry, but I don't think I can do anything here without receiving an assurance that my time here won't be wasted on having to digest more random insults.

[Mario Carneiro]

I would also like to see @Patrick Massot elaborate on what exactly constituted an insult in that PR

[Markus Himmel]

I have opened leanprover-community.github.io#77 and mathlib-tools#63.

[Jalex Stark]

Markus Himmel said:

I have opened leanprover-community.github.io#77 and mathlib-tools#63.

This looks great! Thanks Markus and Dima for the contributions.

[Patrick Massot]

Once again: there is no problem with proposing improved installation instructions. The current instructions are a workaround which is far from being fully satisfactory. The main issue it solves is https://github.com/pypa/pip/issues/3813. Experience so far proves that people who don't have an intensive use of python can use this workaround without trouble, and people who work with python know how to do better (I certainly don't use this workaround myself).

But I'd be very happy to have a better solution, especially in debian_details which is written for Debian/Ubuntu users who actively clicked to see more details about what is going on in the automatic installation. I'm not happy with Dima's "jokes" (since this seems to be the official word here), but this is not a big deal. I should have commented on the tone of the PR instead of closing it immediately, but I was tired yesterday when I saw it. It was 1am here and I should have gone to bed first.

Dima, I really don't think your style of communication is helpful, but hopefully you can still have fun with Lean and maybe even bring interesting things here.

[Patrick Massot]

The pipx thing seems interesting, I didn't know about it. Did anyone tried it? If yes then I'd happily recommend it in the detailed instructions. However it somehow feels more intrusive to use in the automatic procedure.

[Markus Himmel]

Patrick Massot said:

Did anyone tried it?

I use pipx to manage my leanproject installation, and it works perfectly well as far as I can tell.

However it somehow feels more intrusive to use in the automatic procedure.

I see where you're coming from, but to me it also feels intrusive to use a known-suboptimal installation method in the automatic script.

[Dima Pasechnik]

the role of pipx here is pretty limited, it basically makes sure that ~/.local/bin is in your PATH. It certainly is possible to achieve the same in 5-10 lines of bash script, but is it worthwhile? The less code to maintain the better, just let pipx do the heavy lifting.

[Patrick Massot]

Oh, I certainly don't want to maintain code that fiddle with PATH, so using pipx is clearly better than rolling our own.

[Dima Pasechnik]

Patrick Massot said:

Dima, I really don't think your style of communication is helpful, but hopefully you can still have fun with Lean and maybe even bring interesting things here.

Patrick, please note that our communication here goes through multiple language barriers (me being Russian/English/Dutch speaker--- much preferring Dutch directness, while often getting lost in English English politeness) in our heads, and things might get lost or maimed in translation.

As well, please point at the particular comments from me (before the moment you closed the PR #74) that you didn't like. I am always eager to learn to irritate people less.

[Patrick Massot]

I think many people told you what was wrong, the look, no sudo "joke" . I've seen a lot of GH PRs, but I've never seen any PR containing mockery laughing at how the project you want to "contribute to" handles things. People certainly laugh at other people, but usually they're not enough aggressive to PR their mockery to the project they laugh at.

[Patrick Massot]

Crap, I may have merged https://github.com/leanprover-community/leanprover-community.github.io/pull/77 too quickly. When reviewing the companion doc PR I wanted to check that pipx supports Windows, and I noticed they require python 3.6+. Again this is no problem with python users, but we also want to serve people who don't care about python.

[Sebastien Gouezel]

Why should this be a problem? People who don't care about python will just install it to get Lean, and then they will get a recent python.

[Patrick Massot]

I'm afraid of people having a system that already has python 3.5.

[Patrick Massot]

I have now idea what people actually use. Ubuntu has been on python 3.6 since 18.04.

[Patrick Massot]

But python3.5 is not even deprecated by the the python foundation.

[Sebastien Gouezel]

3.6 is there since at least 2017, so I think it's pretty safe.

[Patrick Massot]

What is the situation on Windows? You need to install python by yourself anyway, right?

[Sebastien Gouezel]

Yes.

[Scott Morrison]

Just to add to the multiple languages issues, there's a common phrase in (american?) english: "Look ma, no hands!" (said as if riding a bike) that is often intended in a sort of self-deprecating manner --- that you're both showing off and knowing that it's not important. I won't presume to guess whether the "look, no sudo" phrasing was related to this. Let's all just aim for clear communication and assuming the best of unclear communications. :-)

[Dima Pasechnik]

Patrick Massot said:

I think many people told you what was wrong, the look, no sudo "joke" . I've seen a lot of GH PRs, but I've never seen any PR containing mockery laughing at how the project you want to "contribute to" handles things. People certainly laugh at other people, but usually they're not enough aggressive to PR their mockery to the project they laugh at.

And some people told me they liked the joke. A PR is something that is meant to be changed if needed, something that is often meant for discussion. It's not a direct commit into master. It might have been inappropriate to have it there, and not on this chat, but I bet only you saw it as "mocking the project" and "aggressive".

[Jalex Stark]

what happens to a windows user with python3.5 installed if they try to follow the instructions?

[Dima Pasechnik]

Jalex Stark said:

what happens to a windows user with python3.5 installed if they try to follow the instructions?

then you will see the error message from pipx, as follows https://github.com/pipxproject/pipx/blob/4bb7a23cfa88bfdf0f3651e590ad24e8c1b6d8a1/setup.py#L6

        "Python 3.6 or later is required. "
        "See https://github.com/pipxproject/pipx "
        "for installation instructions."

(hopefully)

[Jalex Stark]

that seems like a good error message

[Jalex Stark]

can pip be used to install newer versions of python? (quick googling suggests no)

[Dima Pasechnik]

Jalex Stark said:

can pip be used to install newer versions of python? (quick googling suggests no)

no, don't think so - but note that Python 3.6 has been released in 2016. Apart from some weird HPC Linux clusters it's probably hard to find Python 3.5 used as the main Python. Even FreeBSD switched to Python 3.7...

[Jalex Stark]

right, I think the only people we are worried about here are windows users. we already give them instructions on how to install "the latest version of python", so I think we should just emphasize that they need 3.6+

[Dima Pasechnik]

Scott Morrison said:

Just to add to the multiple languages issues, there's a common phrase in (american?) english: "Look ma, no hands!" (said as if riding a bike) that is often intended in a sort of self-deprecating manner --- that you're both showing off and knowing that it's not important. I won't presume to guess whether the "look, no sudo" phrasing was related to this. Let's all just aim for clear communication and assuming the best of unclear communications. :-)

I certainly didn't mean anything ill; e.g. it's used in the same way here in discussing of some detail of Python's distutils:
https://mail.python.org/pipermail/distutils-sig/2009-February/011042.html

[Mario Carneiro]

I think it is clear that we should try not to put jokes in official documentation due to the risk of being misunderstood across language and cultural barriers. That said it seems that the misunderstanding is cleared up and we don't need to marginalize anyone for it. I think it is okay to open another PR for the change (or reopen it, if possible) if it is still deemed worthwhile.

[Dima Pasechnik]

Mario Carneiro said:

I think it is clear that we should try not to put jokes in official documentation due to the risk of being misunderstood across language and cultural barriers. That said it seems that the misunderstanding is cleared up and we don't need to marginalize anyone for it. I think it is okay to open another PR for the change (or reopen it, if possible) if it is still deemed worthwhile.

I hope it's cleared up, and also a better version of the ill-fated PR has already been made: leanprover-community.github.io#77

[Mario Carneiro]

I guess Markus Himmel has already PR'd the relevant bits

[Dima Pasechnik]

Markus Himmel said:

I have opened leanprover-community.github.io#77 and mathlib-tools#63.

I just found that Debian 10 has pipx package. While installing pipx via pip is a more universal solution,
probably Debian people might prefer https://packages.debian.org/buster/pipx

[Scott Morrison]

Apologies if this has been discussed before, but could we rename mathlibtools to leanproject? I'm aware that there are some other components of mathlibtools, but leanproject is by far the most important one at this point, and certainly the most important for new users.

[Mario Carneiro]

alternatively, we could move leanproject to a new repo