Zulip Chat Archive

Stream: general

Topic: Simplifying Mathlib install without command line


Hunter Monroe (Apr 28 2021 at 19:34):

I have identified two ways to simplify significantly the Mathlib install while avoiding the command line: (1) as a one-click install, add to the "trylean_windows" what is missing relative to a complete installation: elan.exe and related files, leanproject.exe (a full Python install is not needed, right), and git/bash exe files without GUI; (2) as a second approach, have the users install Git for Windows, VS Code, and the Lean extension, which can then install elan and leanproject.exe (again no need to install Python, right?). Note that the Lean extension can already install elan since version 0.12, but it needs to ask the user to close and reopen VS Code so the path is updated and to offer to install on startup before a .lean file is opened. In addition to simplifying the install, we can elaborate menus for installing lean projects and also allow contributions to mathlib avoiding use of the command line. Are there any reactions to these two approaches?

Patrick Massot (Apr 28 2021 at 19:36):

leanproject uses python.

Eric Wieser (Apr 28 2021 at 20:32):

Does vscode know about leanproject at all?

Eric Wieser (Apr 28 2021 at 20:35):

Note that by far the most frequent type of problems I've seen users have with installing python is that they have multiple installations without knowing it, and end up mixing and matching. Any attempt to bundle python with bits of the lean tooling is likely to make that problem worse not better.

Eric Wieser (Apr 28 2021 at 20:35):

Perhaps if users are really scared of command lines and installation then we should direct them towards gitpod?

Alex J. Best (Apr 28 2021 at 20:52):

Or Patrick's bundled one-click portable vscode if that is still around?

Scott Morrison (Apr 28 2021 at 23:20):

@Hunter Monroe, rather than redesigning the installation process from scratch, how about we first make some improvements that we want anyway: teaching the VSCode extension how to call leanproject to do various simple tasks. (e.g. pull oleans, or delete zombie oleans, from the ctrl-shift-p mena?)

Hunter Monroe (Apr 28 2021 at 23:36):

@Patrick Massot the attached version of leanproject.exe stands alone from Python--I just ran it on a machine without Python. leanproject.exe . I created it with the command "pyinstaller --onefile leanproject.py". I suggest that this .exe file be added to elan, and once that is done, deleting steps from the windows installation page. @Scott Morrison yes adding leanproject calls from the extension is my next task--these can be consolidated into a menu, not just ctrl-shift-p.

Scott Morrison (Apr 28 2021 at 23:38):

Just a note regarding pyinstaller --onefile leanproject.py: the reason I am proposing abandoning the alpine based docker image in #7401 is because exactly this step mysteriously stopped working on alpine. Admittedly it's a weak argument, as the alpine build is pretty baroque in other ways, but just a word of caution adding this as a dependency in our build setup.

Eric Wieser (Apr 28 2021 at 23:39):

Do you have a link to the logs showing that failure?

Scott Morrison (Apr 28 2021 at 23:39):

I agree that removing the dependency on all of python is nice for users; I just fear it's going to be complicated, and encourage you to do the low-hanging fruit that doesn't require very careful testing first. :-)

Scott Morrison (Apr 28 2021 at 23:40):

@Eric Wieser, you can generate the logs locally in any copy of mathlib, using scripts/docker_build.sh.

Eric Wieser (Apr 28 2021 at 23:42):

I only ask because I've had to respond to a handful of pyinstaller issues with my numpy maintainer hat on, and wonder if the failure looks the same

Scott Morrison (Apr 28 2021 at 23:43):

It seems the github module in python has version bumped, which in turn version bumps pynacl, which then wouldn't compile on alpine. I did manage to get that to work again, by changing the lines

FROM six8/pyinstaller-alpine:alpine-3.6-pyinstaller-v3.4 as leanproject-builder

USER root
# install prerequisites
RUN apk update && apk add --no-cache python3 py3-pip py3-virtualenv make

in .docker/alpine/lean/Dockerfile to

FROM six8/pyinstaller-alpine as leanproject-builder

USER root
# install prerequisites
RUN apk update && apk add --no-cache python3 python3-dev py3-pip py3-virtualenv make

but then although pyinstaller --onefile claims to succeed, leanproject itself doesn't work with error message

#6 0.304 Traceback (most recent call last):
#6 0.304   File "leanproject", line 5, in <module>
#6 0.304 ImportError: No module named mathlibtools.leanproject
#6 0.304 [8] Failed to execute script leanproject

At that point I decided I didn't care enough about having an alpine image...

Hunter Monroe (Apr 29 2021 at 06:15):

@Scott Morrison here is a first peek at leanproject commands added to the VS Code Extension Command Palette Ctrl-Shift P. This still requires another day of work to consolidate these into menus, which need to be located carefully (some commands create projects while others assume you are already editing a project), handle user input for get/new/pr commands (with a menu to get for key lean projects), and provide a menu specific to mathlib contributors (as an alternative to command line actions). In the screenshot, notice the list of Leanproject commands up top and also the terminal output for delete-zombies at the bottom: Leanproject-commands.png

Yaël Dillies (Apr 29 2021 at 07:05):

If these commands make their way onto the widget, don't miss out on the opportunity to insert a zombie icon!

Hunter Monroe (Apr 30 2021 at 15:28):

@Sebastian Ullrich would you support the idea of including leanproject.exe (a standalone version that does not require Python) with elan?

Hunter

Patrick Massot the attached version of leanproject.exe stands alone from Python--I just ran it on a machine without Python. leanproject.exe . I created it with the command "pyinstaller --onefile leanproject.py". I suggest that this .exe file be added to elan, and once that is done, deleting steps from the windows installation page. Scott Morrison yes adding leanproject calls from the extension is my next task--these can be consolidated into a menu, not just ctrl-shift-p.

Scott Morrison (Apr 30 2021 at 15:33):

I don't really understand how it would be possible, without a radical shake-up of the two projects. leanproject is clearly downstream of elan (leanproject is useless without lean already installed), so including an artifact from leanproject back in elan seems like a nightmare from the point of view of testing/CI/reliability.

Sebastian Ullrich (Apr 30 2021 at 15:33):

Yes, shipping elan with leanproject instead seems like the more sensible approach

Hunter Monroe (Apr 30 2021 at 16:04):

Scott and Sebastian, given that python/pip are no longer needed to install leanproject.exe which is just a single file, how are you proposing to install it and where? We have the opportunity to delete two steps from the famously painful installation process: Get Python and Get Scripts: https://leanprover-community.github.io/install/windows.html

Eric Wieser (Apr 30 2021 at 18:34):

We could build a leanproject.exe as part of the mathlib-tools CI?

Eric Wieser (Apr 30 2021 at 18:35):

Or lower short-term effort, just upload such a file manually to the github release page

Eric Wieser (Apr 30 2021 at 18:37):

I also have in the past found having the full python install of mathlibtools valuable as it provides Python API to build on top of - so I don't think we should eliminate the existing distribution method for users who already have python set up

Scott Morrison (May 01 2021 at 00:42):

I think the right solution is to add building and testing leanproject.exe as continuous integration in the mathlibtools project. If It reliably and automatically builds and uploads to github, then we can update the mathlib install instructions for windows with this as an option.

Scott Morrison (May 01 2021 at 00:44):

We should also do the same for non-windows systems (I think the majority of our users?). I know the pyinstaller --onefile does work on other systems, although it is unreliable with respect to upgrades --- this is why I recently abandoned the alpine docker image. This is why I'm saying that we don't really have leanproject.exe yet: we have a proof of concept that it can be done, not a CI setup that generates it.

Hunter Monroe (May 01 2021 at 05:30):

Just to note we have flexibility in that: (1) the elan install is called by a .sh script https://github.com/leanprover/elan/blob/master/elan-init.sh which can do absolutely anything including downloading leanprover.exe from the mathlib-tools github site, and (2) elan has a self update feature "elan update" (on demand). Are there plans to elaborate mathlibtools and elan functionality, and is there any way to check downloads by Windows vs other OS?

Scott Morrison (May 01 2021 at 06:23):

Certainly these install scripts already detect the operating system and decide what to do.

Scott Morrison (May 01 2021 at 06:27):

Re: (1), yes elan can do anything, but if the process over in mathlib-tools CI that was building leanproject.exe broke, suddenly elan-init.sh doesn't work anymore. I'm not the maintainer of either elan or leanproject, but I don't think they would be happy with this situation. Each tool needs to have a continuous integration process that checks that it works. Installing leanproject.exe via elan introduces a circular dependency.

Kevin Buzzard (May 01 2021 at 08:15):

Another issue is that elan is in some sense run by the lean people and leanproject is run by the mathlib people who are downstream from them

Ryan Lahfa (May 01 2021 at 10:09):

BTW, there has been this complain which I think is relevant but not super easy to tackle: https://twitter.com/andrejbauer/status/1388242383498797059

Sebastian Ullrich (May 01 2021 at 10:28):

I don't understand that complaint

Sebastian Ullrich (May 01 2021 at 10:29):

But I wouldn't mind a Homebrew formula for elan

Scott Morrison (May 01 2021 at 10:36):

What's not inspectable? The installation instructions tell you to curl various scripts, and pipe them to the shell. Piping them to stdout is always allowed...

Ryan Lahfa (May 01 2021 at 10:41):

I think it is more: "I do not want to spend time trusting what you wrote, I just want to trust my local package manager" and the way we wrote the things as "wget | curl" (not exactly that, but you can get this feeling)

Sebastian Ullrich (May 01 2021 at 10:48):

It's not like the Homebrew maintainers will review our code either, is it?

Ryan Lahfa (May 01 2021 at 10:55):

Sebastian Ullrich said:

It's not like the Homebrew maintainers will review our code either, is it?

I don't really know what are their practices, but I frequently review Nix derivations (notably Lean ones) in nixpkgs for example.

Sebastian Ullrich (May 01 2021 at 10:57):

...that they are properly packaged, but not that their code is trustworthy, I assume

Ryan Lahfa (May 01 2021 at 10:58):

Sebastian Ullrich said:

...that they are properly packaged, but not that their code is trustworthy, I assume

Right, and, here, I believe the point was trusting the "package installation" code rather than Lean/elan/mathlib code.

Ruben Van de Velde (May 01 2021 at 10:59):

Don't all package managers allow running arbitrary code as part of installation (and update)?

Ryan Lahfa (May 01 2021 at 11:00):

Ruben Van de Velde said:

Don't all package managers allow running arbitrary code as part of installation (and update)?

Nix & Guix don't AFAIK.

Ryan Lahfa (May 01 2021 at 11:00):

e.g. Installation & update process is sandboxed (as long as you didn't disable it), network access is disabled.

Hunter Monroe (May 02 2021 at 03:51):

So @Scott Morrison the next step is to create/modify continuous integration for leanproject to create executables for each platform--who can do that and can I help?

Scott Morrison said:

We should also do the same for non-windows systems (I think the majority of our users?). I know the pyinstaller --onefile does work on other systems, although it is unreliable with respect to upgrades --- this is why I recently abandoned the alpine docker image. This is why I'm saying that we don't really have leanproject.exe yet: we have a proof of concept that it can be done, not a CI setup that generates it.

Eric Wieser (May 02 2021 at 08:28):

The repository is at https://github.com/leanprover-community/mathlib-tools, you could fork it and investigate getting pyinstaller working in CI for your fork, then PR the changes

Eric Wieser (May 02 2021 at 08:31):

There's a prebuilt action here that may or may not be useful: https://github.com/marketplace/actions/pyinstaller-windows

Hunter Monroe (May 02 2021 at 22:09):

@Scott Morrison I pushed changes to the VS Code extension as you suggested and more, with four new submenus of the editor context (right click) menu: existing ctrl-shift-p tasks (pull oleans, delete zombies), leanproject, elan, and lean (see https://github.com/leanprover/vscode-lean/pull/262). I am looking now at CI workflows to build leanproject.

Scott Morrison said:

how about we first make some improvements that we want anyway: teaching the VSCode extension how to call leanproject to do various simple tasks. (e.g. pull oleans, or delete zombie oleans, from the ctrl-shift-p mena?)```

Hunter Monroe (May 04 2021 at 00:00):

@Eric Wieser I created a PR for mathlib-tools that creates a standalone leanproject.exe, to allow mathlib to be installed in WIndows without installing Python.

Eric Wieser said:

The repository is at https://github.com/leanprover-community/mathlib-tools, you could fork it and investigate getting pyinstaller working in CI for your fork, then PR the changes

Eric Wieser (May 04 2021 at 07:09):

I took a quick skim and kicked off CI (github wanted me to check that as a new contributor you're not mining cryptocurrency)

Hunter Monroe (Jul 08 2021 at 01:09):

@Eric Wieser what is needed to wrap up the pull request to create a precompiled leanproject.exe, removing Python as a dependency on Windows? With that and a few other tweaks to the VS Code extension that I have identified, it should be possible to avoid the command line as @Kevin Buzzard has brought up, with point and click installation of projects.

Kevin Buzzard said:

I just want them to get started using Lean in VS Code, and have a system whereby they can easily download a project from GitHub, ideally without having to use the command line at all.

Hunter Monroe (Jul 14 2021 at 18:18):

@Eric Wieser Two months has passed--can this move forward please? Many thanks.

Eric Wieser (Jul 14 2021 at 19:18):

I just looked again, and I think the thing I was worried about is a non-issue

Eric Wieser (Jul 14 2021 at 19:20):

There's one comment I'd like you to add to an existing file, but I think otherwise it looks ok to me

Hunter Monroe (Jul 14 2021 at 23:14):

Thanks I added the two comments. I appreciated the thorough review process. I will come back on a VS Code welcome page and other tweaks that should allow a command line free install.

Eric Wieser (Jul 15 2021 at 00:54):

@Patrick Massot, would you mind giving the PR a final review? Are there documentation pages that should be updated to reference it (even if only as "There is an experimental binary available at ...")

Patrick Massot (Jul 15 2021 at 08:01):

I'll have a look since you ask, but I know nothing about Windows. But indeed this effort will be useless if it's not mentioned in the documentation. That would be a PR in the lean community website.

Eric Wieser (Jul 15 2021 at 08:21):

I only ask since in my mind you're the de-facto steward of that repo. But if you've no experience with windows I could just pull the trigger myself.

Eric Wieser (Jul 15 2021 at 15:26):

(is that +1 a "yes pull the trigger" or "I appreciate that you asked"?)

Patrick Massot (Jul 15 2021 at 17:00):

Both!

Hunter Monroe (Aug 16 2021 at 23:33):

Is there a reason this PR has not been accepted? Another 1 1/2 months has passed.

Johan Commelin (Aug 17 2021 at 06:05):

@Eric Wieser :ping_pong:

Eric Wieser (Aug 17 2021 at 10:34):

I just merged this, but it now fails CI because the requirements.txt is out of date

Eric Wieser (Aug 17 2021 at 10:37):

Hopefully leanprover-community/mathlib-tools#110 will fix it

Eric Wieser (Aug 17 2021 at 11:14):

@Hunter Monroe, do you plan to PR new windows installation instructions now?

Hunter Monroe (Oct 24 2021 at 00:12):

@Eric Wieser To update the windows installation instructions, we need put the artifact leanproject.exe where the user can find it, for instance, by creating a release using the automatic release action. Is this the right approach?

Hunter Monroe (Feb 22 2022 at 19:06):

@Eric Wieser how do we put leanproject.exe where the user can find it? I have been out of touch and may not know the current state of play.

Eric Wieser (Feb 22 2022 at 19:25):

I've no idea what the best approach there is, I'm not really convinced handing users a binary is more accessible than telling them to install it with a package manager like pip. The shorter answer is "let the user decide, and tell them to put thle location they choose on their path". Maybe pyinstaller supports a global install of some kind that can modify the system path, but I know little about it, and suspect it's not worth the trouble.

Hunter Monroe (Feb 22 2022 at 19:55):

@Kevin Buzzard how important would it be to have a one click install of Lean and mathlib—is that still the obstacle it used to be? As a first step I found a way to avoid installing Python on Windows, but we need a way for the user to put leanproject.exe on their path. I have an approach to allow a one click install, but do not want to make a further investment of my time until I am sure that the work already done has not been wasted.

Kevin Buzzard (Feb 22 2022 at 20:36):

I have had no trouble with my course this term and I suspect that this might be because the installation instructions are now pretty solid and cover lots of situations. Won't we all be using lean 4 in a few months?

Patrick Massot (Feb 22 2022 at 20:42):

Yes, I think it doesn't make much sense to invest a lot of time in the Lean 3 install story now. Hopefully in Lean 4 all the tooling will be written in Lean and python won't be involved.

Hunter Monroe (Feb 24 2022 at 01:19):

That makes sense, but I hope the Lean 4 install will not otherwise require use of the command line.


Last updated: Dec 20 2023 at 11:08 UTC