Zulip Chat Archive

Stream: new members

Topic: pre-compiling mathlib

Greg Conneen (May 28 2019 at 06:32):

I just got my new host up and running, and I'm very happy with performance. However, I no longer have mathlib already compiled on this machine, and I completely forget how to go about doing that. Could someone walk me through that process? I'd like for mathlib files to not take quite so long to parse anymore.

Johan Commelin (May 28 2019 at 06:32):

What OS?

Johan Commelin (May 28 2019 at 06:33):

There should be helpful info here: https://github.com/leanprover-community/mathlib#installation

Greg Conneen (May 28 2019 at 06:37):

Windows 2019 datacenter

Johan Commelin (May 28 2019 at 06:37):

Ok, then I can't help (-;

Johan Commelin (May 28 2019 at 06:37):

But maybe that link can still help

Greg Conneen (May 28 2019 at 06:37):

Great, thank you

Sebastien Gouezel (May 28 2019 at 06:43):

Here is the way I do it, which is probably not the recommended way but works fine (I have done it a few weeks ago on my new Windows 10 machine):

  • download the release from https://github.com/leanprover/lean/releases/tag/v3.4.2, install it and make it available in your path
  • install git
  • in a shell, do : git clone https://github.com/leanprover-community/mathlib.git
  • go to the mathlib subdirectory, and create there a file leanpkg.path containing the two lines
builtin_path
path ./src
  • in the mathlib subdirectory, do : lean --make

Johan Commelin (May 28 2019 at 06:44):

This means manually compiling all of mathlib, right?

Johan Commelin (May 28 2019 at 06:44):

He should be able to get a precompiled mathlib

Sebastien Gouezel (May 28 2019 at 06:44):

Yes. With my connection, this is faster than downloading it over the internet :)

Sebastien Gouezel (May 28 2019 at 06:45):

Slow connection, but fast computer :)

Greg Conneen (May 28 2019 at 06:47):

I'm currently overseas accessing my server remotely. My connection is pretty bad. This is the solution I was looking for

Johan Commelin (May 28 2019 at 06:48):

Your connection doesn't matter. What matters is the connection between your server and github

Greg Conneen (May 28 2019 at 06:52):

Unfortunately that's the connection that's slow

Greg Conneen (May 28 2019 at 06:52):

I mentioned I'm overseas because if I were there I could fix my internet

Johan Commelin (May 28 2019 at 06:53):

Ooh, ok. It's not some VPS that you are renting?

Greg Conneen (May 28 2019 at 06:56):

No, it's my device. I usually just use it for managing websites, discord bot scripts, and running simulations, but it's the only thing with compute power that I can access from Japan. So I sorta turned it into a work machine

Last updated: Dec 20 2023 at 11:08 UTC