Simplifying Mathlib install without command line

Stream: general

[Hunter Monroe]

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]

leanproject uses python.

[Eric Wieser]

Does vscode know about leanproject at all?

[Eric Wieser]

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]

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

[Alex J. Best]

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

[Scott Morrison]

@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]

@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]

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]

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

[Scott Morrison]

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]

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

[Eric Wieser]

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]

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]

@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]

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

[Hunter Monroe]

@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]

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]

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

[Hunter Monroe]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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]

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]

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]

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]

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

[Scott Morrison]

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]

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]

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

@XenaProject @leanprover The installation instructions are written for people who are willing to download arbitrary code and run it without inspecting it. I am not one of those people. It would be super cool if Homebrew installation of elan were available.

- Andrej Bauer (@andrejbauer)

[Sebastian Ullrich]

I don't understand that complaint

[Sebastian Ullrich]

But I wouldn't mind a Homebrew formula for elan

[Scott Morrison]

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]

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]

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

[Ryan Lahfa]

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]

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

[Ryan Lahfa]

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]

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

[Ryan Lahfa]

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]

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

[Hunter Monroe]

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]

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]

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

[Hunter Monroe]

@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]

@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]

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]

@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]

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

[Eric Wieser]

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

[Eric Wieser]

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]

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]

@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]

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]

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]

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

[Patrick Massot]

Both!

[Hunter Monroe]

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

[Johan Commelin]

@Eric Wieser :ping_pong:

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Hunter Monroe]

@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]

@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]

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]

@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]

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]

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]

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