Install documentation

Stream: general

[Patrick Massot]

Installation documentation sounds like a more interesting topic to me. I'm currently installing a fresh Xubuntu in VirtualBox. I'll try to follows the instruction and use the remote install script without adding any step to what is written. Wish me good luck...

[Patrick Massot]

But I can already see there are too many steps, and install scripts try to be too generic. What about trying to write a single bash file installing everything assuming a Debian-like OS?

[Patrick Massot]

I think even https://github.com/leanprover-community/mathlib/blob/master/docs/elan.md is too generic. Every step mixes all OS. Shouldn't we write three separate files?

[Johan Commelin]

Two of the files are really easy:

1. Install Linux
2. See the appropriate installation instructions.

[Patrick Massot]

I get a completely random error when using curl https://raw.githubusercontent.com/leanprover-community/mathlib/master/scripts/remote-install-update-mathlib.sh -sSf | sh. It work flawlessly on my actual machine. In the virtual machine I get one line 28: illegal option -n.

[Johan Commelin]

Try piping through bash

[Patrick Massot]

I tried that

[Patrick Massot]

Then nothing happens (no error, no installation)

[Johan Commelin]

Aha, that is probably because it is asking you redirected stdin a question

[Johan Commelin]

so curl bla > script.sh; yes | bash ./script.sh

[Keeley Hoek]

Does the $PATH happen to be empty on that virtual machine Patrick?

[Johan Commelin]

Keeley, then it would already fail on curl

[Keeley Hoek]

Oh but if the path is empty most normal shells check a default path and could find curl

[Patrick Massot]

In this case we don't want to install script to answer the question.

[Patrick Massot]

$PATH is not empty

[Patrick Massot]

The question is coming from the remote-install-update-mathlib.sh script itself

[Johan Commelin]

So

curl the_script > script.sh
./script.sh

and let the user answer questions.

[Patrick Massot]

The weird thing is: I say it works here. But it doesn't ask any question here

[Patrick Massot]

Oww: the python install downloads 200Mo

[Patrick Massot]

Of course most of it should be already there on a real computer

[Johan Commelin]

Especially on a computer that has Lean and its tools up and running (-;

[Patrick Massot]

I can confirm that downloading the remote install script first and executing it behaves as intended

[Patrick Massot]

Then there is this annoying requests warning, but I know how to get rid of it

[Patrick Massot]

And then everything works

[Patrick Massot]

elan manages to download, launch and ask questions in one line. We need investigations

[Johan Commelin]

And then everything works

Including update-mathlib and the git hooks etc...?

[Patrick Massot]

Including update-mathlib. I don't think git-hooks should be enabled by default

[Johan Commelin]

Why not?

[Patrick Massot]

Because it makes git slow as hell

[Simon Hudon]

I thought overall it would save time

[Patrick Massot]

Maybe I'm using it wrong

[Patrick Massot]

also, someone needs to find time for an obvious bug fix: currently we query GitHub for existence of a nightly before checking the local hard drive

[Patrick Massot]

it's not only a matter of permuting two lines, because we need to figure out the name of the olean archive we are looking for. But it shouldn't be hard

[Simon Hudon]

Yeah, I looked into it a while back. It's hard to fix because the name of the archive is the date, not the sha of the commit. We would need to change this convention which might break the setup of a bunch of people

[Patrick Massot]

This is what I feared, and the reason why I haven't try yet

[Simon Hudon]

Maybe we could create a file mapping dates to commit sha

[Simon Hudon]

... or we could have a bunch of symbolic links to the archives and name them after the sha that they correspond to

[Patrick Massot]

Hey the install question eaten by bash is the same as https://github.com/leanprover-community/mathlib/pull/940

[Patrick Massot]

The more I thought about it, the more it reminded me something

[Patrick Massot]

Is there any good reason to instruct user to pipe the remote install script through sh instead of bash?

[Patrick Massot]

Is bash installed on MacOS for instance?

[Johan Commelin]

They are still stuck with bash 3.4.2 though...

[Johan Commelin]

Linux has had bash 4 for ages.

[Patrick Massot]

What about bash read?

[Patrick Massot]

Do they have it on MacOS?

[Johan Commelin]

Je ne sais pas

[Patrick Massot]

I guess Git-bash includes enough of bash for this to work

[Patrick Massot]

@Simon Hudon I just opened https://github.com/leanprover-community/mathlib/pull/968 about all this

[Patrick Massot]

As soon as this gets merged, I'll ask VirtualBox to jump back in time and try again following instructions on a fresh Ubuntu

[Patrick Massot]

I really think there is no other way to test this. Even Travis includes too much in its default install

[Simon Hudon]

It looks good. Does that affect how you call curl to install it?

[Simon Hudon]

I think Travis is already better than nothing. I wish we could test it better though. Especially with Windows because I don't have a Windows machine and I don't know when I'll break the setup of Windows users

[Patrick Massot]

I don't know anything about Windows, but I have an evil plan. Now that I installed VirtualBox, I intend to ask the computer staff here if my university is paying Windows for me anyway (this could very well be the case). If yes then I'm ready to install Windows in virtual box (yes, this is how devoted I am)

[Patrick Massot]

About curl. The way we tell people to use curl does not work. It never worked on systems that don't have python3 with pip already

[Patrick Massot]

With my PR, I believe it works as long as you replace sh by bash at the end of the line

[Patrick Massot]

To be more precise: in https://github.com/leanprover-community/mathlib/blob/master/scripts/remote-install-update-mathlib.sh#L28 this is assuming the bash version of read is used. Those option simply don't exist in POSIX

[Johan Commelin]

Patrick, I'm really worried. Maybe you should go see a doctor...

[Patrick Massot]

I should have gone for vacations with my family instead of working all week long

[Johan Commelin]

Aah, on sh vs bash... we should also fix all the shebang lines

[Patrick Massot]

But I'm really tired of people fighting to install Lean/mathlib

[Patrick Massot]

The shebang lines are not used anyway

[Patrick Massot]

if you follow the instructions

[Johan Commelin]

But a user might end up using them...

[Johan Commelin]

So they better be correct

[Patrick Massot]

The instructions never say "download this, make it executable, execute"

[Johan Commelin]

But a security-minded user might still do that (after inspecting the file contents with $EDITOR)

[Patrick Massot]

true

[Patrick Massot]

Let me push one more commit then

[Johan Commelin]

They will know how to fix the shebang line... but it would be a nice service to do that for them

[Patrick Massot]

done

[Simon Hudon]

Sorry to ask for another commit but can we get the README.md to reflect what you just explained about curl?

[Patrick Massot]

Ok, I can do that right now, but I intend to revamp this as soon as I'll get confirmation it works on a bare Ubuntu install

[Patrick Massot]

done

[Johan Commelin]

Now wait 1hr for Travis to approve, and you'll know (-;

[Johan Commelin]

Or we can be evil and just hit the "merge" button.

[Patrick Massot]

I've already stopped and restored my virtual machine

[Patrick Massot]

I think this will be faster that Travis

[Johan Commelin]

Btw, I just read about https://developers.google.com/season-of-docs

[Patrick Massot]

Travis just completed checking the first commit (out of 3)

[Johan Commelin]

We're using software by evil microsoft... might as well have it documented by evil google...

[Johan Commelin]

Travis just completed checking the first commit (out of 3)

It already gave up on the 2nd

[Patrick Massot]

Why?

[Johan Commelin]

Je ne sais pas

[Patrick Massot]

@Simon Hudon would you mind merging right now? This way I could test on my virtual machine before leaving my office

[Patrick Massot]

I guess I'm being overly cautious here. I can replace the branch in the url and pretend it was merged

[Patrick Massot]

Note: Travis fails the olean-rs stage, nothing to do with my changes...

[Simon Hudon]

done

[Patrick Massot]

So weird. I just tried (before the merge) in a fresh Ubuntu, and the script stopped after installing python3 and pip.

[Patrick Massot]

Everything else worked flawlessly

[Patrick Massot]

I'm shutting down my VM, restoring, trying again with the official merged version

[Patrick Massot]

same result :sad:

[Simon Hudon]

What's the instruction after that install?

[Patrick Massot]

execution should jump to https://github.com/leanprover-community/mathlib/blob/master/scripts/remote-install-update-mathlib.sh#L57

[Patrick Massot]

which is a pip3 install

[Patrick Massot]

relauching the script works

[Patrick Massot]

so something's wrong inside the part that is executed when pip is not there

[Patrick Massot]

it almost looks like both lines 31 and 33 are executed

[Simon Hudon]

Can you add a print statement after the fi on line 34?

[Patrick Massot]

I have no idea what's going on here. But there is a fix. The whole list of instructions starts with: type sudo apt install git curl, so we can add python3 and python3-pip to that list

[Patrick Massot]

Ok, I'll try that

[Simon Hudon]

:+1:

[Patrick Massot]

Indeed that print is effective

[Simon Hudon]

What if you put it at the end of the whole if ... fi?

[Simon Hudon]

(after fi)

[Patrick Massot]

which one?

[Patrick Massot]

54 or 55?

[Patrick Massot]

I'll try all of them

[Simon Hudon]

yes please

[Patrick Massot]

this is completely crazy

[Patrick Massot]

now apt aborts

[Patrick Massot]

Actually it was strange that it didn't wait for confirmation inside apt when it was half working

[Patrick Massot]

I hope you admire how I resists the temptation to suggests replacing bash with a proper programation language

[Simon Hudon]

Bash is so horrible even Python is better. Go for it if it helps ... except ... aren't you trying to install Python?

[Patrick Massot]

Yes, I'm acutely aware of this time-travel paradox

[Patrick Massot]

I tried something that seemed to work

[Simon Hudon]

Then go for it. Just don't sleep with your grandmother

[Simon Hudon]

What did you do?

[Patrick Massot]

I added the -y to apt-get. We are asking for confirmation right before doing it anyway

[Patrick Massot]

And miraculously it then worked until the end of the install procedure...

[Simon Hudon]

What happens at the end?

[Patrick Massot]

What I call the end is everything starting from line 57

[Patrick Massot]

https://github.com/leanprover-community/mathlib/blob/master/scripts/remote-install-update-mathlib.sh#L57

[Patrick Massot]

/me shuts down his, VM, restore, rinse, repeat

[Simon Hudon]

setuptools seem to be giving a hard time to pip

[Patrick Massot]

bash seems to be giving a hard time to bash

[Simon Hudon]

"stop hitting yourself! stop hitting yourself!"

[Patrick Massot]

PR'ed again

[Patrick Massot]

An idea for future improvement: maybe update-mathlib should propose to run leanpkg add leancommunity/mathlib if it can't find mathlib in leanpkg.toml

[Patrick Massot]

I'm hungry, I'll leave my office. I did almost nothing than working on mathlib installation for the past three hours

[Simon Hudon]

That's frustrating

[Simon Hudon]

Is your PR ready to merge?

[Patrick Massot]

Yes, I hope so

[Patrick Massot]

After getting some food I'll work on README.md and elan.md

[Patrick Massot]

It's frustrating but if it's worth the trouble if the installation indeed becomes easy

[Simon Hudon]

Indeed

[Kevin Buzzard]

Yes absolutely. Even a few weeks ago at Obergurgl it was painful to install mathlib, which was a shame. It would be great if it were really simple by the time of "Big Proof" at the end of this month

[Simon Hudon]

I don't think "simple" is a concrete goal. I think it keeps getting simpler. What specifically do you want it to be like by the end of the month?

[Kevin Buzzard]

My experience at AITP was: someone handed me a mac and I followed the instructions in the mathlib README. I typed the curl line and it didn't work to install update-mathlib. I piped everything to a file and ran it, and this did work but then update-mathlib didn't work on the version of mathlib we'd just downloaded, so I had to go to my computer, find a commit hash which I knew update-mathlib would work for, git checkout that commit and then do it. It took about 20 minutes in total.

Whilst I was doing that, someone with some non-standard linux was trying to install it as well, but when they tried update-mathlib they had the wrong python or the wrong pip or something, and ended up having to upgrade their entire system to fix the problem -- it was "something they'd been meaning to do for months" but still.

[Patrick Massot]

"simple" has a very concrete meaning on Debian-like systems. It means sudo apt install lean, wait 30 seconds and then use the software. Having a simple installation procedure means getting closer to this definition of simple. I think copy pasting a curl ... | bash is almost good enough

[Patrick Massot]

We're not there yet

[Patrick Massot]

People used to Debian are probably spoiled children, but we still want them on board. It's a bit unfortunate that they are the same people that will read "If you get stuck, please come to the chat room to ask for assistance.", follow the link, see you need to register on Zulip, and walk away

[Simon Hudon]

How hard would it be to create a lean-mathlib package for apt-get?

[Johan Commelin]

Whilst I was doing that, someone with some non-standard linux was trying to install it as well, but when they tried update-mathlib they had the wrong python or the wrong pip or something, and ended up having to upgrade their entire system to fix the problem -- it was "something they'd been meaning to do for months" but still.

Well... people with non-standard linux are used to hacking their way through intallation instructions. They inflict that upon themselves. (I know this by experience.) I don't think we need to worry about them. They'll be fine (and happy).

[Kevin Buzzard]

Yes, the guy with the non-standard linux took far more than 20 minutes to install mathlib but seemed very happy with the situation at all points. The person with the mac was perplexed that it took so long. They also had to install homebrew or brew or whatever that package manager thing is called.

[Patrick Massot]

How hard would it be to create a lean-mathlib package for apt-get?

There are two very different version of that question.

• Creating a leanmathlib.deb that we could put on a website and tell people: download that file and sudo dpkg -i lean-mathlib.deb. This is very easy. I've done it for my department, so that computer people could deploy Lean in our teaching computer room

• Getting lean in the Debian/Ubuntu repositories is much harder. There are quality requirements here. And it starts with: we should get the source code for Lean and the package must be able to build lean from source. And then someone has to promise to maintain it. It looks easy right now, but wait for Lean 4...

[Patrick Massot]

I'm lying a bit about the first version. I didn't handle elan, only a fixed version of Lean with a fixed version of mathlib

[Johan Commelin]

We've talked about this before I think: and someone said that some big company (like MS) might have people who build and maintain such software packages. That could work really well.

[Johan Commelin]

Also... we'd never want to package mathlib. It is way too rolling release

[Simon Hudon]

What I would do is package the scripts for getting it

[Patrick Massot]

You can still dream of a day where "all elementary stuff" will be in mathlib, and most people won't need to update daily

[Simon Hudon]

But I think the future is a bit too uncertain

[Patrick Massot]

Packaging for Debian wouldn't much sense at this point

[Johan Commelin]

For now I would just focus on providing our own curl bla | bash installer

[Patrick Massot]

yes

[Johan Commelin]

Also, integration with the VScode extension is a big win

[Johan Commelin]

We could extend that...

[Patrick Massot]

Honestly, my plan is the opposite

[Johan Commelin]

Why that?

[Patrick Massot]

I want to include downloading VScode and installing the Lean extension as part of the curl... | bash thing

[Johan Commelin]

You want elan to install VScode (-; :stuck_out_tongue_wink:

[Simon Hudon]

I think that's reasonable

[Simon Hudon]

Also, I would include a --emacs option

[Patrick Massot]

I tried on real students: finding that extension icon you need to click is far more difficult than copy-paste something in a terminal

[Johan Commelin]

Also, I would include a --emacs option

There are no options... only different curl bla | bash lines.

[Simon Hudon]

Indeed :P

[Patrick Massot]

I see half of my students on Tuesday and half on Friday. During the first week I can tell you I spend my Wednesday creating screenshots to distribute to students

[Johan Commelin]

Or maybe a question...

Do you want
 (i)  VScode or
 (ii) (((super-(world-(domination))-editor) Emacs))?

[Patrick Massot]

I wouldn't even bother. People who will prefer emacs over VScode can take care of themselves

[Johan Commelin]

Right... they fall in the same category as "non-standard Linux"-users

[Simon Hudon]

I think we can have an easy path for the emacs user but I wouldn't ask most user what editor they want

[Jesse Michael Han]

emacs users can just grab it off MELPA (is there a similar solution for the community fork of lean-mode?)

[Johan Commelin]

What is "it"? We're talking about installing VScode + elan + update-mathlib... + all dependencies

[Johan Commelin]

But I agree that emacs users will probably be savvy enough about their system to figure out how to get what they want.

[Johan Commelin]

And otherwise there is always C-M-Butterfly

[Jesse Michael Han]

oh, i meant emacs lean-mode

[Jesse Michael Han]

one might have to manually set the path to the lean executable though

[Simon Hudon]

It's not on Melpa but it could be. It needs polishing though

[Kevin Buzzard]

I would like a one-liner for ubuntu / debian which installs VS Code and Lean and mathlib and makes a project with mathlib as a dependency and a file in src called test with a proof that 2 + 2 = 4, and all the olean files, and makes update-mathlib work and git too. I don't care about it automatically keeping up to date. But if anyone in Edinburgh says "so how do I compile this schemes project?" I can just say "type this command"

[Patrick Massot]

I hope you will have it tomorrow

[Kevin Buzzard]

And I'm worried about python and pip

[Patrick Massot]

We are still talking about Debian/Ubuntu, right?

[Kevin Buzzard]

Right

[Kevin Buzzard]

But I guess it would be nice if it worked on a Mac too...

[Kevin Buzzard]

For a one off installation we could just dump all the mathlib olean files in with the lean files -- but then I think there are issues with timestamps

[Patrick Massot]

I'm pretty sure it's also east on a Mac, we only need to find one (this is much easier than finding a Windows, but still non-trivial)

[Andrew Ashworth]

If you've already decided to use virtual box, Microsoft offers isos at https://www.microsoft.com/en-gb/software-download/windows10ISO

[Andrew Ashworth]

You do not need to activate, you'll just get a nag screen

[Patrick Massot]

Oh, that's crazy! How can this work? Anyway, I've asked my computer team, and there should be an official way for me. They are asking (it's a very unusual request...)

[Patrick Massot]

I worked on the Debian side. This is crazily time-consuming, I spent more than two extra hours on this, but I now propose https://github.com/leanprover-community/mathlib/pull/974

[Patrick Massot]

Featuring the one line to rule them all: https://github.com/leanprover-community/mathlib/blob/debian/docs/install_debian.md

[Johan Commelin]

I really like the example project that you suggest in your tutorial (-;

[Patrick Massot]

It's replacing lean-stacks-project which is currently in the general documentation

[Bryan Gin-ge Chen]

The last few steps of your instructions can be simplified: you can open the current working directory in VS Code by typing code . instead of code. Would you mind if I edited this into your branch?

[Patrick Massot]

I never managed to get code . to behave this way

[Bryan Gin-ge Chen]

Oh, that's strange. Never mind then.

[Patrick Massot]

And I'm not sure we want to hide how to open a folder in VScode. In my teaching experience, that's the most frequent source of confusion for students (far more confusing than type class search or coercions).

[Patrick Massot]

No matter how often I tell them where to put files and what folder to open, I still have to go around the computer room to fix this

[Patrick Massot]

(France no longer has a mandatory military year for 18 years old men. So giving a list of instruction to follow without thinking does not work on first year university students)

[Jesse Michael Han]

The install instructions should be updated to reflect the migration of the scripts to mathlib-tools (I was walking someone through the install instructions 5 minutes ago)

[Jesse Michael Han]

PR'd

[Jesse Michael Han]

the URLs inside remote-install-update-mathlib.sh need to be updated too

[Patrick Massot]

I was complaining about this one hour ago, but needed to go get my children