I'm going to automate the Lean & Mathlib installation

Stream: general

[Daniel Donnelly]

I love Lean. More so more than CoqIDE. However, I would like an all-encompassing IDE that installs everything you need with one EXE download. To begin with, I am going to automate the installation instructions found here:
https://leanprover-community.github.io/install/windows.html
Using Selenium WebDriver (which I have a lot of skill with) and PyWinAuto. Does anyone suggest an alternative approach to having an auto installer such as "there is an upcoming Lean version and installation is way different or easier".
Thank you.

[Johan Commelin]

@Daniel Donnelly have you seen https://leanprover-community.github.io/get_started.html#maybe-a-couple-of-nights ?

[Daniel Donnelly]

@Johan Commelin "The downside is you won't be able to create your own projects or easily upgrade Lean and mathlib. You'll need a regular install for this." Can't really make use of that

I'm going to create a PyQt5 App GUI which has an InstallerThread doing the install instructions. It will even click the download link on the GitForWindows page for example. I'll try to make it cross platform, but I'll have to finish the Linux / MacOS branches secondly.

[Johan Commelin]

Well, on linux I always use the one line installation command. Works like a charm.

[Daniel Donnelly]

@Johan Commelin where's a link to info on that?

[Johan Commelin]

Ok, it's for Debian-based distros only: https://leanprover-community.github.io/install/debian.html

[Johan Commelin]

But also the generic linux install is, what I would call "straightforward"

[Daniel Donnelly]

@Johan Commelin Okay, I will make one for windows / macOS then

[Johan Commelin]

If I were you I would also search this Zulip for all the issues that people have been hitting. (Preinstalled different Python, wrong $PATH, other stuff.) Because if 1-click install sounds great. But if it cannot handle all those edges cases it just becomes an opaque box that only works if the stars align.

[Johan Commelin]

And someone needs to troubleshoot all those installation issues.

[Daniel Donnelly]

@Johan Commelin that sounds like a good idea. The automator will try to always add to path, which usually works unless the length of path is too long. It will do this by always checking the box in the Python installer. Once I start working on my IDE I will have the option to not add to path as I can just store location info with the IDE's program files. Or if I figure out a way to install everything without adding Python to the Path, the first version will also have that option

[Johan Commelin]

I don't know what your IDE is going to do... will it be a full-fledged frontend to git and leanproject? Sounds like a lot of work. Without them, you are back to the "maybe a couple of days" that I linked to above.

[Johan Commelin]

But with Lean 4 around the corner, leanproject is probably going to change a lot. So building an IDE around it, I dunno.

[Johan Commelin]

Personally, I don't think it helps to hide git and leanproject behind a bunch of menu items.

[Daniel Donnelly]

"Without them" - not sure what you mean here

[Johan Commelin]

Because as soon as there is some complicated operation, it's not supported by the menu, and you need to fall back to a terminal anyway

[Daniel Donnelly]

@Johan Commelin So you're saying Visual Studio is pointless? I personally can't code without it

[Johan Commelin]

Working on leanprojects implies working with git (and if you don't want to compile lean and mathlib) then you also want elan and leanproject

[Johan Commelin]

Daniel Donnelly said:

Johan Commelin So you're saying Visual Studio is pointless?

What VScode gives me is: a window to type text in, syntax highlighting, a goal window, with widgets, auto-completion.

[Johan Commelin]

Those are all extremely useful.

[Daniel Donnelly]

@Johan Commelin mine will definitely have those.

[Johan Commelin]

But how do you get mathlib caches for your lean project?

[Daniel Donnelly]

The whole IDE will be a lot nicer than the VSCode experience. Imagine the simplifications that are possible. Not sure about your question, could you go into more detail with it?

[Johan Commelin]

I'm not saying that what you want isn't useful. I'm warning you that it will be a lot of work that will need to be redone when switching to Lean 4.

[Daniel Donnelly]

@Johan Commelin I am comfortable with that. I might not even get that far into the critical code before Lean 4 is out and about.

[Johan Commelin]

@Daniel Donnelly is your IDE going to use VScode as its main driver?

[Daniel Donnelly]

@Johan Commelin no, either QScintilla as a text editor something custom built using Qt. The main IDE will be written in C++ / Qt Creator.

[Johan Commelin]

Ok, I don't think that's a good idea.

[Daniel Donnelly]

@Johan Commelin why not?

[Johan Commelin]

The lean extension for VScode is doing a lot of nontrivial stuff.

[Daniel Donnelly]

@Johan Commelin for example?

[Daniel Donnelly]

Well, anyway, I think Lean is a big enough project now that it deserves its own IDE.

[Johan Commelin]

goal window + widgets. That's extremely powerful. And completely non-trivial to replicate.

[Johan Commelin]

I don't understand what an IDE will do that VScode doesn't.

[Daniel Donnelly]

@Daniel Donnelly Lots of cool features. One thing I wanted to do was display commutative diagrams "wherever possible".

[Daniel Donnelly]

I already have CD display and editing code written in PyQt5. I could make use of it eventually.

[Daniel Donnelly]

@Johan Commelin but the idea is that it will one day be the preferable way to code in Lean because it will be like what Visual Studio's C++ editing and debug support is to the C++ Language.

[Johan Commelin]

I think it's easier to improve the VScode extension than start over from scratch

[Johan Commelin]

Widgets were designed with such "commutative diagram" features in mind.

[Daniel Donnelly]

@Johan Commelin What do you mean by "Widgets" here?

[Johan Commelin]

https://www.edayers.com/thesis/
https://www.youtube.com/watch?v=8NUBQEZYuis&list=PLlF-CfQhukNnO8z3TcFcoKozif9gbl7Yt&index=4

[Daniel Donnelly]

@Johan Commelin thanks for the links.

[Johan Commelin]

@Daniel Donnelly I think I don't really understand why you consider Lean in VScode not to be "IDE experience"

[Johan Commelin]

Lean 4 is providing even more language server integration, so it will only get better

[Daniel Donnelly]

@Johan Commelin I will think about it...

[Daniel Donnelly]

@Johan Commelin that's really interesting how they are coding the widget code in lean itself.

[Johan Commelin]

If you haven't used widgets yet, I would not start writing a new Lean IDE. I think they are unique to Lean, and they are IDE-next-level

[Daniel Donnelly]

@Johan Commelin is there a link for installing the Lean Widgets framework?

[Johan Commelin]

They are installed by default if you use VScode

[Daniel Donnelly]

@Johan Commelin what is important about having the widget code specified in Lean itself?

[Yaël Dillies]

Johan Commelin said:

They are installed by default if you use VScode

*if you use the Lean extension

[Johan Commelin]

@Daniel Donnelly it makes it easy for tactics to create new functionality

[Daniel Donnelly]

@Johan Commelin can't think of a use case. Do you have an example in mind?

[Johan Commelin]

We are still hoping for fancy_rw that allows users to pointy-click on an assumption, and on some part of the goal, and then it rewrites the goal at that point with that assumption

[Johan Commelin]

But I'm not a tactic writer.

[Yaël Dillies]

Oooh, that's an idea? It sounds very cool.

[Johan Commelin]

Also, Lean understands Lean expressions. So turning Lean code for a commutative diagrams into tikzcd code is something probably best done in Lean.

[Yaël Dillies]

More prosaically, I think we could have rw_lhs and rw_rhs as abbreviations for nth_rewrite_lhs 0/nth_rewrite_rhs 0.

[Daniel Donnelly]

Okay, I am liking the idea of just modifying the VSCode ext / using Lean Widgets. I will still write a Windows installer. It will have the option to also automatically install VSCode if you don't already have it. @Yaël Dillies @Johan Commelin

[Daniel Donnelly]

(deleted)

[Yaël Dillies]

That sounds reasonable :smile:

[Johan Commelin]

That installer still needs to support all those edge cases I talked about earlier. And it should make it easier to troubleshoot when things go wrong. It should also make it at least as easy as nowadays for people to execute "complex" git and leanproject combos in a terminal.

[Daniel Donnelly]

@Yaël Dillies does this widget functionality have some documentation?

[Johan Commelin]

I don't think there is low-hanging fruit in the installation procedure.

[Johan Commelin]

Mind you, I don't claim it's optimal either.

[Johan Commelin]

But improving what we have requires taking care of edge cases, and keeping the troubleshooters on Zulip in mind.

[Johan Commelin]

@Daniel Donnelly I don't know too much about the widget implementation, but Ed's thesis that I linked to above is probably the best docs there are.

[Yaël Dillies]

Yeah, he wrote a signficant part (all?) of the widget, so if you had any question he would probably be the best person to ask to.

[Daniel Donnelly]

@Yaël Dillies @Johan Commelin Thank you for the guidance! This definitely put me on a different path, but the better one.

[Daniel Donnelly]

I've bookmarked this conversation to come back to later. First I'll work on installer, then I'll look into Lean Widgets and how to modify the authors code.

[Daniel Donnelly]

I deally, later on I want to enable users to prove stuff by drawing in arrows, and having that data feedback into lean @Yaël Dillies @Johan Commelin

[Kevin Buzzard]

@Daniel Donnelly I would be less inclined to emphasize the git complexities which others have mentioned. For me the main issue is that I'm faced with a mathematics undergraduate with a new laptop they got for going to university, with nothing installed on it (no git no python, no idea what they're doing, no programming experience) and 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.

[Eric Wieser]

There was one piece of low-hanging installation fruit, which was bundling leanproject into an executable to avoid the need to install python. We already have a PR for that though, so the ball in really in the maintainers court.

[Kevin Buzzard]

One problem I have had with undergraduates is that a few months after they've got things working and have got their own project up and running, they want to download another project, so I say "well fire up the command line that you used to install Lean" and they say "I have no idea how to do that and no memory of what I did"

[Daniel Donnelly]

@Kevin Buzzard That's the plan. I can list all github projects in a widget (in the installer) for exmaple

[Eric Wieser]

Kevin, to what extent does gitpod solve that issue?

[Kevin Buzzard]

I don't know because I have not done any work with new undergraduates wanting to install Lean since last Oct/Nov when gitpod didn't exist.

[Marc Huisinga]

fyi, we're still using gitpod for our lean 4 course and so far it works very well

[Eric Wieser]

Do we have gitpod set up for the tutorials project?

[Daniel Donnelly]

Are your undergraduate students usually Windows users?

[Johan Commelin]

Probably yes, since 90% of the world is?

[Daniel Donnelly]

Nice, then Windows support will be first priority :)

[Daniel Donnelly]

@Johan Commelin is there a way to make VS Code look more like a dedicated Lean IDE? I mean by hiding some of the buttons / menus.

[Johan Commelin]

I don't know, but I also don't really care.

[Johan Commelin]

The first thing I do when opening VScode is hit F11

[Johan Commelin]

And then I access whatever I need via the Ctrl-P dropdown menu

[Eric Wieser]

I would argue that having a different IDE for each language is not something I want at all. If I were to ask for one thing to make vscode more lean-y, it would be having a custom file type icon for lean files

[Daniel Donnelly]

@Eric Wieser for that, Lean community first needs to choose an icon :) The "LEAN" text image is not iconizable as is.

[Andrew Ashworth]

I took a look at this a long time ago for Lean 4

[Andrew Ashworth]

As you know Lean is built on Windows with CMake

[Andrew Ashworth]

I am not sure if Lean 4 is still able to be built with Visual Studio

[Andrew Ashworth]

it was an issue for quite some time in Lean 3, but anyway

[Andrew Ashworth]

When I last looked at it, the bootstrap procedure wasn't quite working with my MSYS2 build environment

[Andrew Ashworth]

I think the way to make it easier for Windows non-technical users would be

[Andrew Ashworth]

check that it builds correctly with Visual Studio

[Andrew Ashworth]

using CMake and the new Windows universal CRT

[Andrew Ashworth]

then get a developer certificate and sign the binary, and post it to the Windows store

[Andrew Ashworth]

The double-plus community A+ solution is to extend the CMake build files to use CPack

[Andrew Ashworth]

from CPack you can generate .exe, .dmg, .deb, .rpm, etc with the right configuration for all platforms

[Andrew Ashworth]

Now as for automating mathlib installation - I'm not sure this problem can be solved this way, because we have a catch 22. Some users will want to always use the newest mathlib, and some will want to stick with whatever current version they have. So updating your store package will undoubtedly make one subset somewhat irate

[Andrew Ashworth]

This is something the language package manager really needs to handle. This is something that I heard needs work in Lean 4, so... you could contribute to that, or piggyback on the efforts of existing crossplatform package managers. The biggest and most well known at the moment is probably the Anaconda Python distribution - they handle binaries for numerous Python packages, as well as R.

[Eric Wieser]

As I understand it, the windows store is an application repository, not a package repository. Using it to manage dependencies sounds miles from its intended use case.

[Mario Carneiro]

I have heard of chocolatey mentioned in discussions of windows package repositories like apt, although I have never used it

[Andrew Ashworth]

avoid Chocolatey, use scoop

[Eric Wieser]

Why do we need any of these things given we have elan?

[Andrew Ashworth]

OP wants a 1-click installer for non-technical users

[Mario Carneiro]

The problem with using these things to install software is that now you have two problems

[Mario Carneiro]

same thing with installing python

[Andrew Ashworth]

Yes

[Andrew Ashworth]

distributing Lean is more like an operating system than an application

[Mario Carneiro]

the only way to 1-click install on windows reliably is to hand the user a .exe

[Alex J. Best]

Andrew Ashworth said:

avoid Chocolatey, use scoop

Can you elaborate? Do you mean in general or just for this topic?

[Andrew Ashworth]

oh, in general. It's too advanced for normal users

[Andrew Ashworth]

both options are as complicated as using apt-get

[Eric Wieser]

I notice that elan says it removed the windows installer which rustup had

[Eric Wieser]

Does adding this back remove the perceived complexity?

[Andrew Ashworth]

I think for non-technical users

[Andrew Ashworth]

what is really needed is a modification to the vscode extension

[Andrew Ashworth]

to add a "package management" tab to the left-hand side activity bar

[Andrew Ashworth]

I have no idea if this is possible, but maybe somebody, somewhere has written a git implementation in javascript or compiled it to webassembly

[Andrew Ashworth]

oh.. as for elan installing a windows toolchain

[Andrew Ashworth]

i don't know. I never used elan, I always built Lean 3 from source

[Andrew Ashworth]

for me personally, I never quite understood elan's target market. You're already in the terminal, so asking someone to run cmake .. && cmake --build && cmake --install always seemed a pretty low ask

[Andrew Ashworth]

and then if you're a non-programmer even opening the terminal is scary and how do you do that??

[Eric Wieser]

Elan's killer feature is that it automatically gets the right version of lean for whatever you're building. I can download a random lean project and build it without having to worry about downloading and building the version of lean it needs by hand

[Eric Wieser]

Vscode has a terminal window

[Andrew Ashworth]

Nobody knows how to use a terminal window. These days people install apps from app stores

[Andrew Ashworth]

Most people's primary computing device is a phone or tablet

[Yakov Pechersky]

Except coding in VSCode is difficult on a phone or tablet keyboard...

[Andrew Ashworth]

True. Let us restrict ourselves to mathematical software, then. Typically users of RStudio, MATLAB, Mathematica - they just click install on their executable and go. There is no such thing as having a rolling release of such software - they get introduced and packaged as a complete whole, usually every 6-12 months

[Andrew Ashworth]

I really think to fix this problem for non-sophisticated users will probably require handholding from the VSCode extension

[Andrew Ashworth]

A command-line tool is too complicated, I think

[Andrew Ashworth]

But you know that is something @Daniel Donnelly would have to decide to work on. I'm just throwing out my 2c cheap opinions here