## Stream: new members

### Topic: Mac installation

#### David Michael Roberts (Oct 08 2018 at 08:51):

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 (Oct 08 2018 at 08:56):

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 (Oct 08 2018 at 09:49):

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

#### Kevin Buzzard (Oct 08 2018 at 10:11):

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 (Oct 09 2018 at 03:35):

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

#### Mario Carneiro (Oct 09 2018 at 05:16):

@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 (Oct 09 2018 at 06:09):

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 (Oct 09 2018 at 06:09):

There's the official instructions of course!

#### Mario Carneiro (Oct 09 2018 at 06:32):

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

#### Scott Morrison (Oct 09 2018 at 06:58):

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 (Oct 09 2018 at 06:59):

(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 (Oct 09 2018 at 06:59):

(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 (Oct 09 2018 at 08:08):

@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 (Oct 09 2018 at 10:49):

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

#### Scott Morrison (Oct 09 2018 at 11:06):

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

#### Kevin Buzzard (Oct 09 2018 at 12:27):

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

#### David Michael Roberts (Oct 10 2018 at 04:51):

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 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 (Oct 10 2018 at 04:51):

It could well be.

#### Scott Morrison (Oct 10 2018 at 04:51):

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

#### Scott Morrison (Oct 10 2018 at 04:51):

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

#### Scott Morrison (Oct 10 2018 at 04:51):

This might mean nothing at all at the moment.

#### Scott Morrison (Oct 10 2018 at 04:52):

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

#### Scott Morrison (Oct 10 2018 at 04:53):

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

:-(

#### Scott Morrison (Oct 10 2018 at 04:54):

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

#### Scott Morrison (Oct 10 2018 at 04:54):

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 (Oct 10 2018 at 04:55):

(We _really_ need to fix this issue.)

#### Mario Carneiro (Oct 10 2018 at 04:55):

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

#### Scott Morrison (Oct 10 2018 at 04:55):

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

#### Mario Carneiro (Oct 10 2018 at 04:55):

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

#### Scott Morrison (Oct 10 2018 at 04:56):

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

#### Scott Morrison (Oct 10 2018 at 04:57):

(I better make another video. :-)

#### David Michael Roberts (Oct 10 2018 at 04:57):

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 (Oct 10 2018 at 04:57):

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 (Oct 10 2018 at 04:58):

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

#### Scott Morrison (Oct 10 2018 at 04:58):

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

#### Mario Carneiro (Oct 10 2018 at 04:58):

I guess, but how close?

#### Scott Morrison (Oct 10 2018 at 04:59):

As often as you can be bothered pushing it?

#### Scott Morrison (Oct 10 2018 at 04:59):

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

#### David Michael Roberts (Oct 10 2018 at 05:01):

Well, that's doing something.

#### David Michael Roberts (Oct 10 2018 at 05:01):

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

Oh ...

#### David Michael Roberts (Oct 10 2018 at 05:02):

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

No.

#### Scott Morrison (Oct 10 2018 at 05:03):

These nightlies are versions of Lean, not of mathlib.

#### Scott Morrison (Oct 10 2018 at 05:03):

mathlib changes most days!

#### Scott Morrison (Oct 10 2018 at 05:03):

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

#### Scott Morrison (Oct 10 2018 at 05:03):

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

Done!

#### David Michael Roberts (Oct 10 2018 at 05:08):

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

#### Kevin Buzzard (Oct 10 2018 at 06:23):

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 (Oct 10 2018 at 06:25):

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 (Oct 10 2018 at 06:27):

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

#### Mario Carneiro (Oct 10 2018 at 06:27):

No, it ties in to the way leanpkg works

#### Mario Carneiro (Oct 10 2018 at 06:27):

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

#### Kevin Buzzard (Oct 10 2018 at 06:28):

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

#### Mario Carneiro (Oct 10 2018 at 06:28):

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

Last updated: May 10 2021 at 00:31 UTC