## Stream: new members

### Topic: lean, elan, leanpkg, leanproject -- documentation?

#### Jasmin Blanchette (Jun 24 2020 at 10:44):

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 (Jun 24 2020 at 10:45):

This has all gone through several iterations.

#### Jasmin Blanchette (Jun 24 2020 at 10:46):

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

#### Kevin Buzzard (Jun 24 2020 at 10:46):

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 (Jun 24 2020 at 10:46):

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

#### Kevin Buzzard (Jun 24 2020 at 10:46):

That's just coming :-)

#### Jasmin Blanchette (Jun 24 2020 at 10:46):

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

#### Jasmin Blanchette (Jun 24 2020 at 10:47):

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

#### Kevin Buzzard (Jun 24 2020 at 10:47):

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

Wow.

#### Jasmin Blanchette (Jun 24 2020 at 10:47):

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

#### Kevin Buzzard (Jun 24 2020 at 10:48):

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

#### Kevin Buzzard (Jun 24 2020 at 10:48):

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

#### Jasmin Blanchette (Jun 24 2020 at 10:48):

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

#### Kevin Buzzard (Jun 24 2020 at 10:49):

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 (Jun 24 2020 at 10:49):

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 (Jun 24 2020 at 10:50):

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 (Jun 24 2020 at 10:51):

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 (Jun 24 2020 at 10:52):

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

#### Jasmin Blanchette (Jun 24 2020 at 10:53):

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 (Jun 24 2020 at 10:54):

The toolchain link is on the install page.

#### Jasmin Blanchette (Jun 24 2020 at 10:56):

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 (Jun 24 2020 at 10:59):

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

#### Jasmin Blanchette (Jun 24 2020 at 11:00):

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 (Jun 24 2020 at 11:10):

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

#### Patrick Massot (Jun 24 2020 at 11:11):

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

#### Patrick Massot (Jun 24 2020 at 11:12):

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 (Jun 24 2020 at 11:13):

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

#### Jasmin Blanchette (Jun 24 2020 at 11:15):

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 (Jun 24 2020 at 11:16):

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

#### Jasmin Blanchette (Jun 24 2020 at 11:17):

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 (Jun 24 2020 at 11:17):

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

#### Kevin Buzzard (Jun 24 2020 at 11:17):

leanproject up should solve your problems

#### Kevin Buzzard (Jun 24 2020 at 11:18):

or in your case leanproject get-cache

#### Kevin Buzzard (Jun 24 2020 at 11:31):

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 (Jun 24 2020 at 11:53):

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

#### Jasmin Blanchette (Jun 24 2020 at 11:53):

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

#### Jasmin Blanchette (Jun 24 2020 at 11:54):

Thanks for the help!

#### Rob Lewis (Jun 24 2020 at 12:06):

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 (Jun 24 2020 at 12:31):

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

#### Jasmin Blanchette (Jun 24 2020 at 12:32):

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

#### Jasmin Blanchette (Jun 24 2020 at 12:32):

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

#### Patrick Massot (Jun 24 2020 at 14:48):

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 (Jun 24 2020 at 15:03):

@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 (Jun 24 2020 at 17:08):

@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 (Jun 24 2020 at 17:09):

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 (Jun 24 2020 at 17:12):

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

#### Patrick Massot (Jun 29 2020 at 22:22):

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

#### Patrick Massot (Jun 29 2020 at 22:23):

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

#### Kevin Buzzard (Jun 29 2020 at 22:26):

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

#### Dima Pasechnik (Jun 29 2020 at 22:27):

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 (Jun 29 2020 at 22:34):

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 (Jun 29 2020 at 22:37):

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

#### Kevin Buzzard (Jun 29 2020 at 22:58):

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

#### Alex J. Best (Jun 29 2020 at 23:01):

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 (Jun 29 2020 at 23:06):

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 (Jun 29 2020 at 23:13):

Insulting us won't improve things.

#### Dima Pasechnik (Jun 29 2020 at 23:15):

Patrick Massot said:

Insulting us won't improve things.

excuse me? how am i insulting anyone here?

#### Dima Pasechnik (Jun 29 2020 at 23:16):

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?

jeez...

#### Dima Pasechnik (Jun 29 2020 at 23:18):

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 (Jun 29 2020 at 23:19):

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

#### Jalex Stark (Jun 29 2020 at 23:20):

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

#### Dima Pasechnik (Jun 29 2020 at 23:21):

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 (Jun 29 2020 at 23:23):

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

#### Dima Pasechnik (Jun 29 2020 at 23:23):

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 (Jun 29 2020 at 23:24):

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 (Jun 29 2020 at 23:25):

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

#### Jalex Stark (Jun 29 2020 at 23:25):

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 (Jun 29 2020 at 23:27):

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 (Jun 29 2020 at 23:27):

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

#### Jalex Stark (Jun 29 2020 at 23:28):

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 (Jun 29 2020 at 23:30):

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 (Jun 29 2020 at 23:30):

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 (Jun 29 2020 at 23:31):

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 (Jun 29 2020 at 23:32):

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 (Jun 29 2020 at 23:33):

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 (Jun 29 2020 at 23:34):

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

#### Jalex Stark (Jun 29 2020 at 23:35):

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

#### Dima Pasechnik (Jun 29 2020 at 23:37):

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 (Jun 29 2020 at 23:37):

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 (Jun 29 2020 at 23:38):

Many departments issue people laptops without sudo rights, too.

#### Dima Pasechnik (Jun 29 2020 at 23:42):

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

#### Jalex Stark (Jun 29 2020 at 23:46):

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 (Jun 30 2020 at 00:21):

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 (Jun 30 2020 at 03:56):

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 (Jun 30 2020 at 04:06):

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 (Jun 30 2020 at 04:07):

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 (Jun 30 2020 at 04:07):

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 (Jun 30 2020 at 08:19):

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 (Jun 30 2020 at 08:25):

Wheels within wheels! :-)

#### Dima Pasechnik (Jun 30 2020 at 09:19):

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

It is

#### Dima Pasechnik (Jun 30 2020 at 09:20):

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 (Jun 30 2020 at 09:21):

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

#### Dima Pasechnik (Jun 30 2020 at 09:36):

Johan Commelin said:

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

ah, OK.

#### Dima Pasechnik (Jun 30 2020 at 09:42):

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 (Jun 30 2020 at 09:46):

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

#### Sebastien Gouezel (Jun 30 2020 at 09:48):

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 (Jun 30 2020 at 10:15):

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 (Jun 30 2020 at 11:20):

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

#### Markus Himmel (Jun 30 2020 at 15:43):

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

#### Jalex Stark (Jun 30 2020 at 15:47):

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 (Jun 30 2020 at 21:35):

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 (Jun 30 2020 at 21:36):

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 (Jul 01 2020 at 07:09):

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 (Jul 01 2020 at 09:17):

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 (Jul 01 2020 at 09:24):

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 (Jul 01 2020 at 09:29):

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 (Jul 01 2020 at 09:38):

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 (Jul 01 2020 at 09:40):

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 (Jul 01 2020 at 09:43):

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 (Jul 01 2020 at 09:43):

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

#### Patrick Massot (Jul 01 2020 at 09:44):

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

#### Patrick Massot (Jul 01 2020 at 09:44):

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

#### Sebastien Gouezel (Jul 01 2020 at 09:44):

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

#### Patrick Massot (Jul 01 2020 at 09:45):

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

Yes.

#### Scott Morrison (Jul 01 2020 at 09:46):

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 (Jul 01 2020 at 09:52):

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 (Jul 01 2020 at 09:57):

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

#### Dima Pasechnik (Jul 01 2020 at 10:01):

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 (Jul 01 2020 at 10:02):

that seems like a good error message

#### Jalex Stark (Jul 01 2020 at 10:04):

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

#### Dima Pasechnik (Jul 01 2020 at 10:08):

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 (Jul 01 2020 at 10:09):

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 (Jul 01 2020 at 10:13):

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 (Jul 01 2020 at 10:13):

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 (Jul 01 2020 at 10:16):

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 (Jul 01 2020 at 10:16):

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

#### Dima Pasechnik (Jul 01 2020 at 10:23):

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 (Jul 01 2020 at 10:36):

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 (Jul 01 2020 at 10:46):

alternatively, we could move leanproject` to a new repo

Last updated: May 18 2021 at 17:44 UTC