Restarting file in Mathematics in Lean

Stream: new members

[Trevor Karn]

Hi all, I'm new here. I am just starting to work through the Mathematics in Lean book using VS Code. When I close VS code, I have to restart the file, and so various libraries need to get rebuilt. I am surprised at this because I haven't pulled anything from the main branch that I would expect to change and need to get rebuilt. (I'm experienced using Git, but not Lean or VS Code.) Is there something I'm doing wrong that I can do so that I don't have to rebuild Mathlib every time I close VS code?

(Sorry if this is the wrong place to post this, but if it is, would you please redirect me to the correct place? Thanks!)

[Yaël Dillies]

Have you used lake exe cache get?

[Trevor Karn]

I have not. I'll try that. What does it do?

[Yaël Dillies]

As you have noticed, Lean files need building in order to be imported. We don't want everyone to have to build everything, so the Lean FRO is kindly paying a server storing the result of the builds of all major Lean libraries. lake exe cache get fetches those results.

[Trevor Karn]

Ah I see. Thanks Lean FRO! I see that I need to run lake exe cache get in the same directory as my local copy of Mathematics in Lean. Should I take this to mean that if I want to use Lean in another project, then I would also need to run lake exe cache get in the directory of the project I want to work on?

[Yaël Dillies]

Yes, and you will also need to run it every time you change the version of one of the major Lean libraries you're using

[Trevor Karn]

Got it that makes sense. I have run lake exe cache get and restarted VS Code, but I am still getting a message that the libraries are out of date and need to be rebuilt.

[Yaël Dillies]

Try Ctrl + Shift + X, let it run for 30 seconds and see

[Trevor Karn]

Thanks for the suggestion. Nothing seems to have changed. I do see

info: [1037/1963] Building Mathlib.Algebra.Star.SelfAdjoint

in the Lean Infoview window

[Yaël Dillies]

Did you already get things rebuilt before posting here for help?

[Trevor Karn]

I had previously built them successfully, yesterday or the day before, but not yet today

[Trevor Karn]

I guess I was hoping that I was just doing something dumb and I could add some configuration option when bulding in order to avoid having to build again. If I understand, it seems like using the lake cache is supposed to accomplish that goal?

[Yaël Dillies]

What environment are you in? Your computer? Gitpod? Codespaces?

[Sebastian Ullrich]

Trevor Karn said:

Thanks for the suggestion. Nothing seems to have changed. I do see

info: [1037/1963] Building Mathlib.Algebra.Star.SelfAdjoint

in the Lean Infoview window

Is that a slow or a fast progress counter? I.e. seconds or hours?

[Trevor Karn]

Yaël Dillies said:

What environment are you in? Your computer? Gitpod? Codespaces?

Computer

[Trevor Karn]

Sebastian Ullrich said:

Trevor Karn said:

Thanks for the suggestion. Nothing seems to have changed. I do see

info: [1037/1963] Building Mathlib.Algebra.Star.SelfAdjoint

in the Lean Infoview window

Is that a slow or a fast progress counter? I.e. seconds or hours?

It seems to be slow. At this point several minutes, not yet an hour

[Trevor Karn]

Yaël Dillies said:

What environment are you in? Your computer? Gitpod? Codespaces?

I haven't used Gitpod or Codespaces before. Do you prefer one over the other?

[Yaël Dillies]

I highly rate gitpod, especially because they give 250h/month free if you tell them you contribute to free software (which this community is)

[Yaël Dillies]

I haven't tried codespaces

[Trevor Karn]

It turns out that it takes < 10 min to get Mathematics in Lean running on VS code in Gitpod. This seems like a good option when it is taking longer than that to build locally on my machine.

[Trevor Karn]

Trevor Karn said:

Sebastian Ullrich said:

Trevor Karn said:

Thanks for the suggestion. Nothing seems to have changed. I do see

info: [1037/1963] Building Mathlib.Algebra.Star.SelfAdjoint

in the Lean Infoview window

Is that a slow or a fast progress counter? I.e. seconds or hours?

It seems to be slow. At this point several minutes, not yet an hour

It did take several hours on my previous build.

[Sebastian Ullrich]

You didn't post the cache output on the cmdline, did it say it was 100% successful?

[Trevor Karn]

Sebastian Ullrich said:

You didn't post the cache output on the cmdline, did it say it was 100% successful?

(base) trevorkarn@MacBook-Air-196 mathematics_in_lean % lake exe cache get
Warning: recommended `curl` version ≥7.70. Found 7.68.0. Can't use `--parallel`.
No files to download
Decompressing 4198 file(s)
unpacked in 9422 ms

This is what I got

[Trevor Karn]

I didn't see the phrase "successful" in there, but I am interpreting it to be good other than my outdated curl. Does that seem right?

[Ruben Van de Velde]

It does seem good, yeah

[Trevor Karn]

Thanks everyone for all of your help with this. I decided to try starting over from scratch, following the directions here https://leanprover-community.github.io/install/project.html#working-on-an-existing-project diligently. When I get to the lake cache step I get the following output

trevorkarn@MacBook-Air-196 mathematics_in_lean % lake exe cache get
info: mathlib: cloning https://github.com/leanprover-community/mathlib4 to '././.lake/packages/mathlib'
info: std: cloning https://github.com/leanprover/std4 to '././.lake/packages/std'
info: Qq: cloning https://github.com/leanprover-community/quote4 to '././.lake/packages/Qq'
info: aesop: cloning https://github.com/leanprover-community/aesop to '././.lake/packages/aesop'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to '././.lake/packages/proofwidgets'
info: Cli: cloning https://github.com/leanprover/lean4-cli to '././.lake/packages/Cli'
info: importGraph: cloning https://github.com/leanprover-community/import-graph.git to '././.lake/packages/importGraph'
Attempting to download 1 file(s)
Downloaded: 0 file(s) [attempted 1/1 = 100%] (0% success)
Warning: some files were not found in the cache.
This usually means that your local checkout of mathlib4 has diverged from upstream.
If you push your commits to a branch of the mathlib4 repository, CI will build the oleans and they will be available later.
Decompressing 4449 file(s)
unpacked in 74247 ms

Does anyone know why the local checkout of mathlib4 would have diverged from upstream, especially when it looks like the upstream was just cloned?

[Trevor Karn]

And, can I ask, is there an easy way to tell which file is the one that download failed on?

[Trevor Karn]

When I opened VS Code the first time, it seemed to build the missing file (took ~3 min), and now the "rebuilding" step takes a very short amount of time when I restart VS Code.

[Ruben Van de Velde]

Can you run lean --version and paste the output here?

[Trevor Karn]

trevorkarn@MacBook-Air-196 mathematics_in_lean % lean --version
Lean (version 4.8.0-rc1, x86_64-apple-darwin22.6.0, commit dcccfb73cb24, Release)

[Ruben Van de Velde]

That's good. Unfortunately that means I still don't have a clue

[Ruben Van de Velde]

Even worse, I'm now hitting it on a new clone of flt-regular

[Mario Carneiro]

the easy way to find out which file is missing is to run lake build

[Mario Carneiro]

...although with the new lake output issue (lean4#4069) it may not be so easy anymore

[Ruben Van de Velde]

Maybe Mathlib.NumberTheory.NumberField.Basic

[Ruben Van de Velde]

At least, that's the one that stays on screen for a while

[Trevor Karn]

When I run lake build it seems to build a bunch of Math in Lean files, not any Mathlib files. It is a sort of long output, should I post it here?

[Trevor Karn]

Ruben Van de Velde said:

At least, that's the one that stays on screen for a while

Can you say more what you mean by this? On which screen do you see it?

[Ruben Van de Velde]

I opened a new file and put import Mathlib in it. Then ctrl+shift+x to tell vs code that it's ok to rebuild the missing dependencies. Then the infoview flickered through [X/X] Building Mathlib....

[Ruben Van de Velde]

And that was the first module name that remained fixed for long enough to see it

[Trevor Karn]

Gotcha! When I do the same it seems like [4450/4451] Building Mathlib.Util.Time sticks around for the longest