Mac installation

Stream: new members

[David Michael Roberts]

I notice @Scott Morrison put up a nice short video on getting required dependencies, VS Code and Lean installed on Mac, here: https://www.youtube.com/watch?v=k8U6YOK7c0M

[Kevin Buzzard]

I also rewrote my cheap Windows installation page: https://xenaproject.wordpress.com/a-cheap-hack-to-get-lean-and-mathlib-running-on-a-windows-10-machine/ . I intend over the next day or two to make a link at the top of my blog pointing to various installation pages / posts, which are now randomly scattered online.

[Scott Morrison]

I'm still going to make the corresponding video for installation on Windows!

[Kevin Buzzard]

Be sure to ping me when you do. I am expecting this question to come up a fair bit at Imperial over the next few weeks

[Scott Morrison]

Okay, the video for installing on Windows 10 is now up! https://www.youtube.com/watch?v=2f_9Zetekd8&feature=youtu.be

[Mario Carneiro]

@Kevin Buzzard Would it be possible for you to write a page for mathlib that links to the various tutorials and videos for installing lean and/or mathlib?

[Kevin Buzzard]

I will try to find the time today. On this thread we have Scott's two videos, there are my cheap and less cheap blog posts, there is some elan link somewhere... Is that it?

[Kevin Buzzard]

There's the official instructions of course!

[Mario Carneiro]

It would also be good to have follow on instructions for people who followed Scott's instructions and want mathlib

[Scott Morrison]

Yes, I was thinking that's a separate video, that applies equally on Windows and macos, because it happens entirely within VS Code.

[Scott Morrison]

(That's part of the reason for setting up a usable terminal on Windows, so afterwards everything can be done from VS Code.)

[Scott Morrison]

(Although it occurs to me the Windows video should have included that one extra step, to hook up git bash as the default terminal instead of powershell.)

[Johan Commelin]

@Neil Strickland This thread contains two videos with installation instructions. Kevin is also updating his instructions. Would you mind adding links to these videos etc on your MO post? I think you pointed out a very good issue (that installation was horribly difficult). I also hope that we are addressing them now. What do you think?

[David Michael Roberts]

Maybe the windows video should go in its own topic, for ease of finding?

[Scott Morrison]

Hopefully there will be permanent links to these soon from more prominent places...

[Kevin Buzzard]

I am just going to have an "installing lean" link at the top of my blog with multiple options

[David Michael Roberts]

OK, so I have actually installed Lean and VS code as per @Scott Morrison 's video, and now want to do some mathlibbing. But I am told by @Kevin Buzzard 's post https://xenaproject.wordpress.com/2017/12/02/how-to-install-mathlib-and-keep-it-up-to-date/ that I probably am better off with the nightly build of lean, so that mathlib will have the latest and greatest stuff. After following the instructions at that post:

leanpkg new my_project
cd my_project
leanpkg add https://github.com/leanprover/mathlib
leanpkg build

I get

davidroberts$ leanpkg build
configuring my_project 0.1
mathlib: trying to update _target/deps/mathlib to revision 905345a2ceaa5d0c7bc2f6310026961416b2cae4
> git checkout --detach 905345a2ceaa5d0c7bc2f6310026961416b2cae4    # in directory _target/deps/mathlib
HEAD is now at 905345a fix(data/array/lemmas,...): fix build
> lean --make src

and this was much much quicker than I thought it would be. Is it working or no?

[Scott Morrison]

It could well be.

[Scott Morrison]

leanpkg build, and lean --make src don't compile all of mathlib

[Scott Morrison]

They only compile those parts of it which are imported by some file in src/.

[Scott Morrison]

This might mean nothing at all at the moment.

[Scott Morrison]

Add a file under src/ that imports, e.g. data.nat.prime.

[Scott Morrison]

However, what you did _still_ doesn't get you the latest and greatest version of mathlib.

[Scott Morrison]

:-(

[Scott Morrison]

If you look up that git commit hash you'll see it's from June 21.

[Scott Morrison]

This is because leanpkg is taking you to the latest commit on the lean-3.4.1 branch, which for some reason (@Mario Carneiro ?) never gets updated?

[Scott Morrison]

(We _really_ need to fix this issue.)

[Mario Carneiro]

Don't blame me, Kevin wanted it to stay still

[Scott Morrison]

To get the actual latest version, you should edit your leanpkg.toml file.

[Mario Carneiro]

I guess it points to something like the earliest commit compatible with 3.4.1?

[Scott Morrison]

And replace the line lean_version = ... with lean_version = "nightly-2018-08-23".

[Scott Morrison]

(I better make another video. :-)

[David Michael Roberts]

Aha, doing leanpkg build after adding a file to src/containing import data.nat.prime (plus an #eval 2+2) makes it do a lot more

[David Michael Roberts]

And replace the line lean_version = ... with lean_version = "nightly-2018-08-23".

ah, ok! I'll do that once the current build has finished

[Scott Morrison]

I wonder if @Kevin Buzzard cares about where lean-3.4.1 points, anymore.

[Scott Morrison]

If he doesn't, do you think we can keep it closer to master, @Mario Carneiro ?

[Mario Carneiro]

I guess, but how close?

[Scott Morrison]

As often as you can be bothered pushing it?

[Scott Morrison]

Have a script that keeps it right up to master??

[David Michael Roberts]

Well, that's doing something.

[David Michael Roberts]

Question: why the nightly from the 21st of June?

[Scott Morrison]

Oh ...

[David Michael Roberts]

Is that the 'latest and greatest' version of mathlib?

[Scott Morrison]

No.

[Scott Morrison]

These nightlies are versions of Lean, not of mathlib.

[Scott Morrison]

mathlib changes most days!

[Scott Morrison]

I've just edited my instruction above. You should use nightly-2018-08-23.

[Scott Morrison]

(And maybe even edit your message above where you quoted me, so we can completely rewrite history. :-)

[David Michael Roberts]

Done!

[David Michael Roberts]

I now have nightly-2018-08-23, thanks!

[Kevin Buzzard]

The "you're better off with the nightly build" comment was from when Lean 3.4 was changing a lot, and mathlib would change to keep up with Lean. This is all much less of an issue nowadays.

[Kevin Buzzard]

Don't blame me, Kevin wanted it to stay still

I wanted it to stay still between June and September. Thank you very much Mario for making it stay still over my summer project. I now really really don't want it to stay still any more for the simple reason that it is causing constant confusion amongst users.

[Kevin Buzzard]

Can we just delete the branch @Mario Carneiro or will this cause a new kind of confusion amongst users?

[Mario Carneiro]

No, it ties in to the way leanpkg works

[Mario Carneiro]

I think leanpkg gets even more confused if it's not there at all

[Kevin Buzzard]

I was fearing this. Can we get it to track master somehow?

[Mario Carneiro]

Does someone want to write a git hook so that when I commit to master lean-3.4.1 moves too?