Zulip Chat Archive

Stream: general

Topic: Install documentation


view this post on Zulip 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...

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Johan Commelin (May 02 2019 at 14:18):

Two of the files are really easy:

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 02 2019 at 14:43):

Try piping through bash

view this post on Zulip Patrick Massot (May 02 2019 at 14:43):

I tried that

view this post on Zulip Patrick Massot (May 02 2019 at 14:44):

Then nothing happens (no error, no installation)

view this post on Zulip Johan Commelin (May 02 2019 at 14:44):

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

view this post on Zulip Johan Commelin (May 02 2019 at 14:44):

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

view this post on Zulip Keeley Hoek (May 02 2019 at 14:49):

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

view this post on Zulip Johan Commelin (May 02 2019 at 14:51):

Keeley, then it would already fail on curl

view this post on Zulip Keeley Hoek (May 02 2019 at 14:52):

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

view this post on Zulip Patrick Massot (May 02 2019 at 14:52):

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

view this post on Zulip Patrick Massot (May 02 2019 at 14:52):

$PATH is not empty

view this post on Zulip Patrick Massot (May 02 2019 at 14:53):

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

view this post on Zulip Johan Commelin (May 02 2019 at 14:54):

So

curl the_script > script.sh
./script.sh

and let the user answer questions.

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 02 2019 at 14:58):

Oww: the python install downloads 200Mo

view this post on Zulip Patrick Massot (May 02 2019 at 14:58):

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

view this post on Zulip Johan Commelin (May 02 2019 at 14:59):

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

view this post on Zulip Patrick Massot (May 02 2019 at 15:05):

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

view this post on Zulip Patrick Massot (May 02 2019 at 15:06):

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

view this post on Zulip Patrick Massot (May 02 2019 at 15:06):

And then everything works

view this post on Zulip Patrick Massot (May 02 2019 at 15:07):

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

view this post on Zulip Johan Commelin (May 02 2019 at 15:07):

And then everything works

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

view this post on Zulip Patrick Massot (May 02 2019 at 15:07):

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

view this post on Zulip Johan Commelin (May 02 2019 at 15:10):

Why not?

view this post on Zulip Patrick Massot (May 02 2019 at 15:11):

Because it makes git slow as hell

view this post on Zulip Simon Hudon (May 02 2019 at 15:14):

I thought overall it would save time

view this post on Zulip Patrick Massot (May 02 2019 at 15:15):

Maybe I'm using it wrong

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 02 2019 at 15:18):

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

view this post on Zulip Simon Hudon (May 02 2019 at 15:18):

Maybe we could create a file mapping dates to commit sha

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 02 2019 at 15:21):

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

view this post on Zulip 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?

view this post on Zulip Patrick Massot (May 02 2019 at 15:41):

Is bash installed on MacOS for instance?

view this post on Zulip Johan Commelin (May 02 2019 at 15:41):

They are still stuck with bash 3.4.2 though...

view this post on Zulip Johan Commelin (May 02 2019 at 15:41):

Linux has had bash 4 for ages.

view this post on Zulip Patrick Massot (May 02 2019 at 15:42):

What about bash read?

view this post on Zulip Patrick Massot (May 02 2019 at 15:42):

Do they have it on MacOS?

view this post on Zulip Johan Commelin (May 02 2019 at 15:43):

Je ne sais pas

view this post on Zulip Patrick Massot (May 02 2019 at 15:43):

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

view this post on Zulip Patrick Massot (May 02 2019 at 15:46):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Simon Hudon (May 02 2019 at 15:48):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 02 2019 at 15:59):

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

view this post on Zulip Patrick Massot (May 02 2019 at 16:00):

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

view this post on Zulip Johan Commelin (May 02 2019 at 16:00):

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

view this post on Zulip Patrick Massot (May 02 2019 at 16:01):

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

view this post on Zulip Patrick Massot (May 02 2019 at 16:01):

The shebang lines are not used anyway

view this post on Zulip Patrick Massot (May 02 2019 at 16:01):

if you follow the instructions

view this post on Zulip Johan Commelin (May 02 2019 at 16:01):

But a user might end up using them...

view this post on Zulip Johan Commelin (May 02 2019 at 16:01):

So they better be correct

view this post on Zulip Patrick Massot (May 02 2019 at 16:01):

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

view this post on Zulip Johan Commelin (May 02 2019 at 16:01):

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

view this post on Zulip Patrick Massot (May 02 2019 at 16:02):

true

view this post on Zulip Patrick Massot (May 02 2019 at 16:02):

Let me push one more commit then

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 02 2019 at 16:03):

done

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 02 2019 at 16:05):

done

view this post on Zulip Johan Commelin (May 02 2019 at 16:07):

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

view this post on Zulip Johan Commelin (May 02 2019 at 16:07):

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

view this post on Zulip Patrick Massot (May 02 2019 at 16:08):

I've already stopped and restored my virtual machine

view this post on Zulip Patrick Massot (May 02 2019 at 16:08):

I think this will be faster that Travis

view this post on Zulip Johan Commelin (May 02 2019 at 16:08):

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

view this post on Zulip Patrick Massot (May 02 2019 at 16:08):

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

view this post on Zulip Johan Commelin (May 02 2019 at 16:08):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 02 2019 at 16:09):

Why?

view this post on Zulip Johan Commelin (May 02 2019 at 16:10):

Je ne sais pas

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 02 2019 at 16:29):

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

view this post on Zulip Simon Hudon (May 02 2019 at 16:29):

done

view this post on Zulip 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.

view this post on Zulip Patrick Massot (May 02 2019 at 16:35):

Everything else worked flawlessly

view this post on Zulip Patrick Massot (May 02 2019 at 16:37):

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

view this post on Zulip Patrick Massot (May 02 2019 at 16:40):

same result :sad:

view this post on Zulip Simon Hudon (May 02 2019 at 16:41):

What's the instruction after that install?

view this post on Zulip Patrick Massot (May 02 2019 at 16:41):

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

view this post on Zulip Patrick Massot (May 02 2019 at 16:41):

which is a pip3 install

view this post on Zulip Patrick Massot (May 02 2019 at 16:42):

relauching the script works

view this post on Zulip Patrick Massot (May 02 2019 at 16:42):

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

view this post on Zulip Patrick Massot (May 02 2019 at 16:43):

it almost looks like both lines 31 and 33 are executed

view this post on Zulip Simon Hudon (May 02 2019 at 16:48):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 02 2019 at 16:49):

Ok, I'll try that

view this post on Zulip Simon Hudon (May 02 2019 at 16:50):

:+1:

view this post on Zulip Patrick Massot (May 02 2019 at 16:51):

Indeed that print is effective

view this post on Zulip Simon Hudon (May 02 2019 at 16:52):

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

view this post on Zulip Simon Hudon (May 02 2019 at 16:52):

(after fi)

view this post on Zulip Patrick Massot (May 02 2019 at 16:53):

which one?

view this post on Zulip Patrick Massot (May 02 2019 at 16:53):

54 or 55?

view this post on Zulip Patrick Massot (May 02 2019 at 16:54):

I'll try all of them

view this post on Zulip Simon Hudon (May 02 2019 at 16:54):

yes please

view this post on Zulip Patrick Massot (May 02 2019 at 16:55):

this is completely crazy

view this post on Zulip Patrick Massot (May 02 2019 at 16:56):

now apt aborts

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Patrick Massot (May 02 2019 at 16:59):

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

view this post on Zulip Patrick Massot (May 02 2019 at 17:00):

I tried something that seemed to work

view this post on Zulip Simon Hudon (May 02 2019 at 17:00):

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

view this post on Zulip Simon Hudon (May 02 2019 at 17:00):

What did you do?

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 02 2019 at 17:01):

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

view this post on Zulip Simon Hudon (May 02 2019 at 17:02):

What happens at the end?

view this post on Zulip Patrick Massot (May 02 2019 at 17:03):

What I call the end is everything starting from line 57

view this post on Zulip Patrick Massot (May 02 2019 at 17:03):

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

view this post on Zulip Patrick Massot (May 02 2019 at 17:03):

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

view this post on Zulip Simon Hudon (May 02 2019 at 17:04):

setuptools seem to be giving a hard time to pip

view this post on Zulip Patrick Massot (May 02 2019 at 17:04):

bash seems to be giving a hard time to bash

view this post on Zulip Simon Hudon (May 02 2019 at 17:05):

"stop hitting yourself! stop hitting yourself!"

view this post on Zulip Patrick Massot (May 02 2019 at 17:09):

PR'ed again

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Simon Hudon (May 02 2019 at 17:12):

That's frustrating

view this post on Zulip Simon Hudon (May 02 2019 at 17:12):

Is your PR ready to merge?

view this post on Zulip Patrick Massot (May 02 2019 at 17:12):

Yes, I hope so

view this post on Zulip Patrick Massot (May 02 2019 at 17:13):

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

view this post on Zulip Patrick Massot (May 02 2019 at 17:13):

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

view this post on Zulip Simon Hudon (May 02 2019 at 17:14):

Indeed

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 02 2019 at 17:58):

We're not there yet

view this post on Zulip 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

view this post on Zulip Simon Hudon (May 02 2019 at 18:03):

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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 02 2019 at 18:23):

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

view this post on Zulip Simon Hudon (May 02 2019 at 18:24):

What I would do is package the scripts for getting it

view this post on Zulip 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

view this post on Zulip Simon Hudon (May 02 2019 at 18:24):

But I think the future is a bit too uncertain

view this post on Zulip Patrick Massot (May 02 2019 at 18:25):

Packaging for Debian wouldn't much sense at this point

view this post on Zulip Johan Commelin (May 02 2019 at 18:25):

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

view this post on Zulip Patrick Massot (May 02 2019 at 18:25):

yes

view this post on Zulip Johan Commelin (May 02 2019 at 18:25):

Also, integration with the VScode extension is a big win

view this post on Zulip Johan Commelin (May 02 2019 at 18:25):

We could extend that...

view this post on Zulip Patrick Massot (May 02 2019 at 18:26):

Honestly, my plan is the opposite

view this post on Zulip Johan Commelin (May 02 2019 at 18:26):

Why that?

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 02 2019 at 18:26):

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

view this post on Zulip Simon Hudon (May 02 2019 at 18:27):

I think that's reasonable

view this post on Zulip Simon Hudon (May 02 2019 at 18:27):

Also, I would include a --emacs option

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Simon Hudon (May 02 2019 at 18:28):

Indeed :P

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 02 2019 at 18:29):

Or maybe a question...

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 02 2019 at 18:30):

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

view this post on Zulip 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

view this post on Zulip 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?)

view this post on Zulip Johan Commelin (May 02 2019 at 19:53):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 02 2019 at 19:54):

And otherwise there is always C-M-Butterfly

view this post on Zulip Jesse Michael Han (May 02 2019 at 19:59):

oh, i meant emacs lean-mode

view this post on Zulip Jesse Michael Han (May 02 2019 at 20:00):

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

view this post on Zulip Simon Hudon (May 02 2019 at 20:00):

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

view this post on Zulip 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"

view this post on Zulip Patrick Massot (May 02 2019 at 20:08):

I hope you will have it tomorrow

view this post on Zulip Kevin Buzzard (May 02 2019 at 20:15):

And I'm worried about python and pip

view this post on Zulip Patrick Massot (May 02 2019 at 20:15):

We are still talking about Debian/Ubuntu, right?

view this post on Zulip Kevin Buzzard (May 02 2019 at 20:42):

Right

view this post on Zulip Kevin Buzzard (May 02 2019 at 20:43):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Andrew Ashworth (May 02 2019 at 23:00):

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

view this post on Zulip Andrew Ashworth (May 02 2019 at 23:01):

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

view this post on Zulip 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...)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 03 2019 at 14:00):

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

view this post on Zulip Patrick Massot (May 03 2019 at 14:02):

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

view this post on Zulip 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?

view this post on Zulip Patrick Massot (May 03 2019 at 14:07):

I never managed to get code . to behave this way

view this post on Zulip Bryan Gin-ge Chen (May 03 2019 at 14:07):

Oh, that's strange. Never mind then.

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip Jesse Michael Han (May 13 2019 at 15:46):

PR'd

view this post on Zulip Jesse Michael Han (May 13 2019 at 15:50):

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

view this post on Zulip Patrick Massot (May 13 2019 at 16:37):

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


Last updated: May 14 2021 at 14:20 UTC