Stream: general

Topic: Install documentation

Patrick Massot (May 02 2019 at 14:12):

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 (May 02 2019 at 14:13):

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 (May 02 2019 at 14:15):

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 (May 02 2019 at 14:18):

Two of the files are really easy:

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


Patrick Massot (May 02 2019 at 14:41):

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 (May 02 2019 at 14:43):

Try piping through bash

I tried that

Patrick Massot (May 02 2019 at 14:44):

Then nothing happens (no error, no installation)

Johan Commelin (May 02 2019 at 14:44):

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

Johan Commelin (May 02 2019 at 14:44):

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

Patrick Massot (May 02 2019 at 14:53):

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

Johan Commelin (May 02 2019 at 14:54):

So

curl the_script > script.sh
./script.sh


and let the user answer questions.

Patrick Massot (May 02 2019 at 14:55):

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

Patrick Massot (May 02 2019 at 14:58):

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

Johan Commelin (May 02 2019 at 14:59):

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

Patrick Massot (May 02 2019 at 15:06):

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

Patrick Massot (May 02 2019 at 15:06):

And then everything works

Patrick Massot (May 02 2019 at 15:07):

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

Johan Commelin (May 02 2019 at 15:07):

And then everything works

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

Patrick Massot (May 02 2019 at 15:07):

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

Why not?

Patrick Massot (May 02 2019 at 15:11):

Because it makes git slow as hell

Simon Hudon (May 02 2019 at 15:14):

I thought overall it would save time

Patrick Massot (May 02 2019 at 15:15):

Maybe I'm using it wrong

Patrick Massot (May 02 2019 at 15:15):

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 (May 02 2019 at 15:16):

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 (May 02 2019 at 15:17):

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 (May 02 2019 at 15:18):

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

Simon Hudon (May 02 2019 at 15:18):

Maybe we could create a file mapping dates to commit sha

Simon Hudon (May 02 2019 at 15:19):

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

Patrick Massot (May 02 2019 at 15:21):

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

Patrick Massot (May 02 2019 at 15:21):

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

Patrick Massot (May 02 2019 at 15:41):

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

Patrick Massot (May 02 2019 at 15:41):

Is bash installed on MacOS for instance?

Johan Commelin (May 02 2019 at 15:41):

They are still stuck with bash 3.4.2 though...

Johan Commelin (May 02 2019 at 15:41):

Linux has had bash 4 for ages.

Patrick Massot (May 02 2019 at 15:42):

Do they have it on MacOS?

Je ne sais pas

Patrick Massot (May 02 2019 at 15:43):

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

Patrick Massot (May 02 2019 at 15:46):

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

Patrick Massot (May 02 2019 at 15:47):

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 (May 02 2019 at 15:48):

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

Simon Hudon (May 02 2019 at 15:48):

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

Simon Hudon (May 02 2019 at 15:49):

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 (May 02 2019 at 15:57):

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 (May 02 2019 at 15:58):

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 (May 02 2019 at 15:58):

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

Patrick Massot (May 02 2019 at 15:59):

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 (May 02 2019 at 15:59):

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

Patrick Massot (May 02 2019 at 16:00):

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

Johan Commelin (May 02 2019 at 16:00):

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

Patrick Massot (May 02 2019 at 16:01):

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

Patrick Massot (May 02 2019 at 16:01):

The shebang lines are not used anyway

Johan Commelin (May 02 2019 at 16:01):

But a user might end up using them...

Johan Commelin (May 02 2019 at 16:01):

So they better be correct

Johan Commelin (May 02 2019 at 16:01):

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

true

Patrick Massot (May 02 2019 at 16:02):

Let me push one more commit then

Johan Commelin (May 02 2019 at 16:02):

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

done

Simon Hudon (May 02 2019 at 16:03):

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

Patrick Massot (May 02 2019 at 16:04):

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

done

Johan Commelin (May 02 2019 at 16:07):

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

Johan Commelin (May 02 2019 at 16:07):

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

Patrick Massot (May 02 2019 at 16:08):

I've already stopped and restored my virtual machine

Patrick Massot (May 02 2019 at 16:08):

I think this will be faster that Travis

Patrick Massot (May 02 2019 at 16:08):

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

Johan Commelin (May 02 2019 at 16:08):

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

Johan Commelin (May 02 2019 at 16:09):

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

It already gave up on the 2nd

Why?

Je ne sais pas

Patrick Massot (May 02 2019 at 16:13):

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

Patrick Massot (May 02 2019 at 16:21):

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

Patrick Massot (May 02 2019 at 16:29):

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

done

Patrick Massot (May 02 2019 at 16:33):

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

Patrick Massot (May 02 2019 at 16:35):

Everything else worked flawlessly

Patrick Massot (May 02 2019 at 16:37):

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

Simon Hudon (May 02 2019 at 16:41):

What's the instruction after that install?

Patrick Massot (May 02 2019 at 16:41):

which is a pip3 install

Patrick Massot (May 02 2019 at 16:42):

relauching the script works

Patrick Massot (May 02 2019 at 16:42):

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

Patrick Massot (May 02 2019 at 16:43):

it almost looks like both lines 31 and 33 are executed

Simon Hudon (May 02 2019 at 16:48):

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

Patrick Massot (May 02 2019 at 16:48):

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 (May 02 2019 at 16:49):

Ok, I'll try that

:+1:

Patrick Massot (May 02 2019 at 16:51):

Indeed that print is effective

Simon Hudon (May 02 2019 at 16:52):

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

Simon Hudon (May 02 2019 at 16:52):

(after fi)

which one?

54 or 55?

Patrick Massot (May 02 2019 at 16:54):

I'll try all of them

Patrick Massot (May 02 2019 at 16:55):

this is completely crazy

now apt aborts

Patrick Massot (May 02 2019 at 16:56):

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

Patrick Massot (May 02 2019 at 16:57):

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

Simon Hudon (May 02 2019 at 16:59):

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

Patrick Massot (May 02 2019 at 16:59):

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

Patrick Massot (May 02 2019 at 17:00):

I tried something that seemed to work

Simon Hudon (May 02 2019 at 17:00):

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

What did you do?

Patrick Massot (May 02 2019 at 17:00):

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

Patrick Massot (May 02 2019 at 17:01):

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

Simon Hudon (May 02 2019 at 17:02):

What happens at the end?

Patrick Massot (May 02 2019 at 17:03):

What I call the end is everything starting from line 57

Patrick Massot (May 02 2019 at 17:03):

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

Patrick Massot (May 02 2019 at 17:03):

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

Simon Hudon (May 02 2019 at 17:04):

setuptools seem to be giving a hard time to pip

Patrick Massot (May 02 2019 at 17:04):

bash seems to be giving a hard time to bash

Simon Hudon (May 02 2019 at 17:05):

"stop hitting yourself! stop hitting yourself!"

PR'ed again

Patrick Massot (May 02 2019 at 17:10):

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 (May 02 2019 at 17:11):

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

Simon Hudon (May 02 2019 at 17:12):

That's frustrating

Yes, I hope so

Patrick Massot (May 02 2019 at 17:13):

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

Patrick Massot (May 02 2019 at 17:13):

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

Indeed

Kevin Buzzard (May 02 2019 at 17:27):

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 (May 02 2019 at 17:29):

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 (May 02 2019 at 17:35):

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 (May 02 2019 at 17:58):

"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 (May 02 2019 at 17:58):

We're not there yet

Patrick Massot (May 02 2019 at 18:00):

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 (May 02 2019 at 18:03):

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

Johan Commelin (May 02 2019 at 18:05):

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 (May 02 2019 at 18:14):

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 (May 02 2019 at 18:15):

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 (May 02 2019 at 18:18):

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 (May 02 2019 at 18:22):

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 (May 02 2019 at 18:23):

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

Simon Hudon (May 02 2019 at 18:24):

What I would do is package the scripts for getting it

Patrick Massot (May 02 2019 at 18:24):

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 (May 02 2019 at 18:24):

But I think the future is a bit too uncertain

Patrick Massot (May 02 2019 at 18:25):

Packaging for Debian wouldn't much sense at this point

Johan Commelin (May 02 2019 at 18:25):

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

yes

Johan Commelin (May 02 2019 at 18:25):

Also, integration with the VScode extension is a big win

Johan Commelin (May 02 2019 at 18:25):

We could extend that...

Patrick Massot (May 02 2019 at 18:26):

Honestly, my plan is the opposite

Why that?

Patrick Massot (May 02 2019 at 18:26):

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

Johan Commelin (May 02 2019 at 18:26):

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

Simon Hudon (May 02 2019 at 18:27):

I think that's reasonable

Simon Hudon (May 02 2019 at 18:27):

Also, I would include a --emacs option

Patrick Massot (May 02 2019 at 18:27):

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 (May 02 2019 at 18:28):

Also, I would include a --emacs option

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

Indeed :P

Patrick Massot (May 02 2019 at 18:29):

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 (May 02 2019 at 18:29):

Or maybe a question...

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


Patrick Massot (May 02 2019 at 18:30):

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

Johan Commelin (May 02 2019 at 18:30):

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

Simon Hudon (May 02 2019 at 18:37):

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 (May 02 2019 at 19:52):

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

Johan Commelin (May 02 2019 at 19:53):

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

Johan Commelin (May 02 2019 at 19:54):

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 (May 02 2019 at 19:54):

And otherwise there is always C-M-Butterfly

Jesse Michael Han (May 02 2019 at 19:59):

oh, i meant emacs lean-mode

Jesse Michael Han (May 02 2019 at 20:00):

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

Simon Hudon (May 02 2019 at 20:00):

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

Kevin Buzzard (May 02 2019 at 20:04):

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 (May 02 2019 at 20:08):

I hope you will have it tomorrow

Kevin Buzzard (May 02 2019 at 20:15):

And I'm worried about python and pip

Patrick Massot (May 02 2019 at 20:15):

We are still talking about Debian/Ubuntu, right?

Right

Kevin Buzzard (May 02 2019 at 20:43):

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

Kevin Buzzard (May 02 2019 at 20:44):

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 (May 02 2019 at 21:11):

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 (May 02 2019 at 23:01):

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

Patrick Massot (May 03 2019 at 13:54):

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 (May 03 2019 at 13:57):

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 (May 03 2019 at 13:58):

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

Johan Commelin (May 03 2019 at 14:00):

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

Patrick Massot (May 03 2019 at 14:02):

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

Bryan Gin-ge Chen (May 03 2019 at 14:06):

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 (May 03 2019 at 14:07):

I never managed to get code . to behave this way

Bryan Gin-ge Chen (May 03 2019 at 14:07):

Oh, that's strange. Never mind then.

Patrick Massot (May 03 2019 at 14:08):

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 (May 03 2019 at 14:08):

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 (May 03 2019 at 14:10):

(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 (May 13 2019 at 15:43):

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)

PR'd

Jesse Michael Han (May 13 2019 at 15:50):

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