Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 10:45):

This has all gone through several iterations.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Jasmin Blanchette (Jun 24 2020 at 10:46):

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

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 10:46):

That's just coming :-)

view this post on Zulip Jasmin Blanchette (Jun 24 2020 at 10:46):

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

view this post on Zulip Jasmin Blanchette (Jun 24 2020 at 10:47):

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

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 10:47):

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

view this post on Zulip Jasmin Blanchette (Jun 24 2020 at 10:47):

Wow.

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 10:47):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 10:48):

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

view this post on Zulip 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.

view this post on Zulip Jasmin Blanchette (Jun 24 2020 at 10:48):

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

view this post on Zulip 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/

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Jasmin Blanchette (Jun 24 2020 at 10:52):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 10:54):

The toolchain link is on the install page.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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? ;)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 11:17):

leanproject up should solve your problems

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 11:18):

or in your case leanproject get-cache

view this post on Zulip 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>

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Jasmin Blanchette (Jun 24 2020 at 11:54):

Thanks for the help!

view this post on Zulip 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 ;)

view this post on Zulip 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.)

view this post on Zulip Jasmin Blanchette (Jun 24 2020 at 12:32):

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

view this post on Zulip Jasmin Blanchette (Jun 24 2020 at 12:32):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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
$ leanproject get-cache [or leanpkg build if there's no cache available]

view this post on Zulip Patrick Massot (Jun 24 2020 at 17:27):

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.

view this post on Zulip Jannis Limperg (Jun 24 2020 at 17:37):

Yes of course, no complaining intended. ;)

view this post on Zulip Patrick Massot (Jun 24 2020 at 18:45):

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

view this post on Zulip Jiekai (Jun 29 2020 at 08:04):

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?

view this post on Zulip Johan Commelin (Jun 29 2020 at 08:05):

Magic

view this post on Zulip Johan Commelin (Jun 29 2020 at 08:06):

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

view this post on Zulip Dima Pasechnik (Jun 29 2020 at 22:06):

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`.

view this post on Zulip Patrick Massot (Jun 29 2020 at 22:22):

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

view this post on Zulip Patrick Massot (Jun 29 2020 at 22:23):

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

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 22:26):

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

view this post on Zulip 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. :-)

view this post on Zulip 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 :-)).

view this post on Zulip Patrick Massot (Jun 29 2020 at 22:37):

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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jun 29 2020 at 23:13):

Insulting us won't improve things.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Dima Pasechnik (Jun 29 2020 at 23:17):

jeez...

view this post on Zulip 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.

view this post on Zulip Jalex Stark (Jun 29 2020 at 23:19):

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

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Dima Pasechnik (Jun 29 2020 at 23:25):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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"?

view this post on Zulip Dima Pasechnik (Jun 29 2020 at 23:34):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Dima Pasechnik (Jun 29 2020 at 23:38):

Many departments issue people laptops without sudo rights, too.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Jun 30 2020 at 08:25):

Wheels within wheels! :-)

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 30 2020 at 09:20):

It is

view this post on Zulip 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!

view this post on Zulip Johan Commelin (Jun 30 2020 at 09:21):

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

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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!).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Markus Himmel (Jun 30 2020 at 15:43):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jul 01 2020 at 09:43):

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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jul 01 2020 at 09:44):

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

view this post on Zulip Sebastien Gouezel (Jul 01 2020 at 09:44):

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

view this post on Zulip Patrick Massot (Jul 01 2020 at 09:45):

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

view this post on Zulip Sebastien Gouezel (Jul 01 2020 at 09:46):

Yes.

view this post on Zulip 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. :-)

view this post on Zulip 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".

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Jalex Stark (Jul 01 2020 at 10:02):

that seems like a good error message

view this post on Zulip Jalex Stark (Jul 01 2020 at 10:04):

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

view this post on Zulip 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...

view this post on Zulip 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+

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 01 2020 at 10:16):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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