Zulip Chat Archive

Stream: new members

Topic: Mac installation


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

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

view this post on Zulip Scott Morrison (Oct 08 2018 at 09:49):

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

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

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

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

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

view this post on Zulip Kevin Buzzard (Oct 09 2018 at 06:09):

There's the official instructions of course!

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

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

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

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

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

view this post on Zulip David Michael Roberts (Oct 09 2018 at 10:49):

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

view this post on Zulip Scott Morrison (Oct 09 2018 at 11:06):

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

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

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

view this post on Zulip Scott Morrison (Oct 10 2018 at 04:51):

It could well be.

view this post on Zulip Scott Morrison (Oct 10 2018 at 04:51):

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

view this post on Zulip Scott Morrison (Oct 10 2018 at 04:51):

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

view this post on Zulip Scott Morrison (Oct 10 2018 at 04:51):

This might mean nothing at all at the moment.

view this post on Zulip Scott Morrison (Oct 10 2018 at 04:52):

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

view this post on Zulip Scott Morrison (Oct 10 2018 at 04:53):

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

view this post on Zulip Scott Morrison (Oct 10 2018 at 04:53):

:-(

view this post on Zulip Scott Morrison (Oct 10 2018 at 04:54):

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

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

view this post on Zulip Scott Morrison (Oct 10 2018 at 04:55):

(We _really_ need to fix this issue.)

view this post on Zulip Mario Carneiro (Oct 10 2018 at 04:55):

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

view this post on Zulip Scott Morrison (Oct 10 2018 at 04:55):

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

view this post on Zulip Mario Carneiro (Oct 10 2018 at 04:55):

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

view this post on Zulip Scott Morrison (Oct 10 2018 at 04:56):

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

view this post on Zulip Scott Morrison (Oct 10 2018 at 04:57):

(I better make another video. :-)

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

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

view this post on Zulip Scott Morrison (Oct 10 2018 at 04:58):

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

view this post on Zulip Scott Morrison (Oct 10 2018 at 04:58):

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

view this post on Zulip Mario Carneiro (Oct 10 2018 at 04:58):

I guess, but how close?

view this post on Zulip Scott Morrison (Oct 10 2018 at 04:59):

As often as you can be bothered pushing it?

view this post on Zulip Scott Morrison (Oct 10 2018 at 04:59):

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

view this post on Zulip David Michael Roberts (Oct 10 2018 at 05:01):

Well, that's doing something.

view this post on Zulip David Michael Roberts (Oct 10 2018 at 05:01):

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

view this post on Zulip Scott Morrison (Oct 10 2018 at 05:02):

Oh ...

view this post on Zulip David Michael Roberts (Oct 10 2018 at 05:02):

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

view this post on Zulip Scott Morrison (Oct 10 2018 at 05:02):

No.

view this post on Zulip Scott Morrison (Oct 10 2018 at 05:03):

These nightlies are versions of Lean, not of mathlib.

view this post on Zulip Scott Morrison (Oct 10 2018 at 05:03):

mathlib changes most days!

view this post on Zulip Scott Morrison (Oct 10 2018 at 05:03):

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

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

view this post on Zulip David Michael Roberts (Oct 10 2018 at 05:04):

Done!

view this post on Zulip David Michael Roberts (Oct 10 2018 at 05:08):

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

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

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

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

view this post on Zulip Mario Carneiro (Oct 10 2018 at 06:27):

No, it ties in to the way leanpkg works

view this post on Zulip Mario Carneiro (Oct 10 2018 at 06:27):

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

view this post on Zulip Kevin Buzzard (Oct 10 2018 at 06:28):

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

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