Stopping VSCode from recompiling mathlib

Stream: new members

[Donald Sebastian Leung]

I just created a new project by executing leanproject new kata, edited leanpkg.toml to contain the following:

[package]
name = "kata"
version = "0.1"
lean_version = "leanprover-community/lean:3.20.0"
path = "src"

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "da66bb81bf0466335bae82077f0c335dfe53aeb3"}

and executed leanproject get-mathlib-cache. I then opened my project folder in VSCode and created a new file Preloaded.lean with the following contents:

import data.equiv.basic data.pnat.basic

The orange bar at the import line stays for well over a minute, and system statistics indicate that CPU usage increases to 100%, with all 4G of RAM and 1.5G of swap (of 2G total) being used in the meantime, suggesting that (parts of) mathlib was being recompiled. How do I stop this from happening? I thought that leanproject get-mathlib-cache used to do the job but maybe I misremembered.

[Patrick Massot]

Why did you edit the leanpkg.toml?

[Donald Sebastian Leung]

The toy Lean examples I use for Codewars have been tested with a version of mathlib from about a week ago and I've just been asked to add an example involving a mathlib dependency. I thought it would be easier to pin mathlib and build my new example on that specific commit instead of running all of my previous examples with the newest mathlib.

But now that I think about it, it would probably be easier to just use the newest mathlib and run all of the existing examples against it, especially considering that none of them have any meaningful dependency on mathlib AFAIK.

[Patrick Massot]

That being said I'm not able to reproduce your issue.

[Patrick Massot]

I did exactly what you wrote and everything works fine.

[Patrick Massot]

What happens if you quit VSCode and type leanproject build in the kata folder?

[Donald Sebastian Leung]

Apologies for the late reply, I used the newest mathlib when constructing my Lean examples as I mentioned earlier, but I realized I had to stick to a fixed mathlib version anyway for updating the Lean content on Codewars in order to ensure reproducibility, and so got another chance to reproduce this issue.

What happens if you quit VSCode and type leanproject build in the kata folder?

I get the following output, produced within a second or two:

Building project kata
configuring kata 0.1
mathlib: trying to update _target/deps/mathlib to revision da66bb81bf0466335bae82077f0c335dfe53aeb3
> git checkout --detach da66bb81bf0466335bae82077f0c335dfe53aeb3    # in directory _target/deps/mathlib
Previous HEAD position was f6836c16f chore(scripts): update nolints.txt (#4547)
HEAD is now at da66bb81b feat(*): preparations for roots of unity (#4322)
> lean --make src
/home/dsleung/Desktop/kata/src/InitialSolution.lean:3:0: warning: declaration 'zero_point_nine_recurring_is_one' uses sorry
/home/dsleung/Desktop/kata/src/Solution.lean:16:48: error: unknown identifier 'one_div_pos_of_pos'
/home/dsleung/Desktop/kata/src/Solution.lean:20:10: error: unknown identifier 'one_div_le_of_one_div_le_of_pos'
/home/dsleung/Desktop/kata/src/Solution.lean:12:0: warning: declaration 'zero_point_nine_recurring_is_one' uses sorry
/home/dsleung/Desktop/kata/src/SolutionTest.lean:1:0: warning: imported file '/home/dsleung/Desktop/kata/src/Solution.lean' uses sorry
propext
classical.choice
quot.sound
[sorry]
external command exited with status 1
Command '['leanpkg', 'build']' returned non-zero exit status 1.

I suppose that means mathlib is not being recompiled in this case (but it still definitely is in VSCode)?

[Donald Sebastian Leung]

Update: Upon returning to VSCode after running leanproject build once, it seems that mathlib is no longer being recompiled. Thanks @Patrick Massot !

[Filippo A. E. Nuccio]

I think my VSCode, or Lean installation, has something really wrong in it; after 5/10 minutes of work it "randomly" (so seems to me, at least) start compiling the whole library. And therefore I cannot work anymore... Is anyone experiencing the same problem? Suggestions?

[Filippo A. E. Nuccio]

I should also add that in "normal times" my whole system seems very slow, each type I make a small modification it takes some 5 to 10 seconds to get to work again, which is a LOOOOONG time if you keep on writing things.

[Kevin Lacker]

I also am seeing frequent over-recompilations. I kill my lean server and restart it pretty often. Usually that fixes it. Otherwise, I switch to master branch, pull, rerun leanproject get-cache, and see if that fixes it. Usually it does - maybe I'm causing these problems by doing something inappropriate with branches, I dunno. If that does fix it then merging the new master into my branch fixes my original problem

[Filippo A. E. Nuccio]

How do you kill your server?

[Kevin Buzzard]

Random library recompilation: some tips are (a) close files you're not working on (b) restart VS Code.

5 to 10 seconds of orange bars: this just sounds like you used an expensive tactic early on in a proof and it is being run again and again. So it's "bad code" in some sense.

[Filippo A. E. Nuccio]

(btw are you also using VSCode? On Win, Mac?)

[Kevin Lacker]

C-c C-r in emacs. Or just with ps aux and kill from a terminal

[Bryan Gin-ge Chen]

In VS Code you can hit ctrl+P (or cmd+P on a mac) and type "Lean: restart". You can also bind a key to this command.

[Filippo A. E. Nuccio]

Kevin Buzzard said:

Random library recompilation: some tips are (a) close files you're not working on (b) restart VS Code.

5 to 10 seconds of orange bars: this just sounds like you used an expensive tactic early on in a proof and it is being run again and again. So it's "bad code" in some sense.

Could very possibly be: what are the typical " bad" tactics? I guess simp is one

[Kevin Lacker]

emacs on linux. vscode isn't doing the recompilation itself, right? it's communicating out to some lean process

[Filippo A. E. Nuccio]

Right

[Filippo A. E. Nuccio]

Bryan Gin-ge Chen said:

In VS Code you can hit ctrl+P (or cmd+P on a mac) and type "Lean: restart". You can also bind a key to this command.

I tried with ctrl+P, the bar when I can write opens but when I type Lean: restart I just get a "No matching result' error... am I missing something?

[Kevin Lacker]

try just typing "Lean" and looking through the options

[Bryan Gin-ge Chen]

Oh sorry, it's ctrl+shift+p

[Filippo A. E. Nuccio]

It restarted but it is compiling everything again. Probably @Kevin Buzzard is right, my code must be terrible

[Kevin Lacker]

is it also recompiling your import statements at the top of the file? or is it only recompiling code that you wrote yourself

[Filippo A. E. Nuccio]

I believe it is recompiling the whole library (there are orange bars on the left, where the library is, and all over the file, from the first line down to where I am writing)

[Scott Morrison]

I would recommend: open a terminal, run leanproject build, then use ctrl-shift-p "Lean: restart".

[Scott Morrison]

If leanproject build is recompiling everything, then either you have edited a file low in hierarchy, and need to either

1. commit your branch and let continuous integration compile everything, or
2. let leanproject build complete locally.

[Filippo A. E. Nuccio]

Scott Morrison said:

I would recommend: open a terminal, run leanproject build, then use ctrl-shift-p "Lean: restart".

Thanks, I had tried this in the afternoon. the leanproject build command took a hour or so (is it normal?), and then Lean worked for some 10/15 minutes. After that, it begun compiling everything again

[Scott Morrison]

If leanproject build returns relatively quickly (say, at most 10s, hopefully much less), and you then restart the lean server and still see orange bars, then we really have a problem.

[Scott Morrison]

No, if you have up-to-date olean then leanproject build should take at most 10s.

[Scott Morrison]

Hopefully less!

[Kevin Lacker]

are you working on a branch of the main repo, or on a fork of the project, or how do you have that set up?

[Filippo A. E. Nuccio]

I am working on a branch of the main repo

[Filippo A. E. Nuccio]

(which is Anne's repo, actually, Vierkantor-dedekind-domain)

[Filippo A. E. Nuccio]

Scott Morrison said:

Hopefully less!

Let me try again!

[Kevin Lacker]

try running leanproject get-cache before building

[Filippo A. E. Nuccio]

I am going to, give me 30 sec

[Filippo A. E. Nuccio]

Now I get an error, but I think this comes from the fact that I have just pull and the server must be compiling

[Bryan Gin-ge Chen]

Which file(s) are you editing, exactly?

[Bryan Gin-ge Chen]

An hour doesn't seem unreasonable if you're editing something really low level.

[Filippo A. E. Nuccio]

BTW: Is this related to the fact that after almost every pull I receive an e-mail with an error saying [leanprover-community/mathlib] Run failed: continuous integration - Vierkantor-dedekind-domain (8bd048d)

[Bryan Gin-ge Chen]

You can turn those notifications off from your GitHub settings.

[Filippo A. E. Nuccio]

Bryan Gin-ge Chen said:

Which file(s) are you editing, exactly?

I am editing the file on Dedekind Domains, I don't think it is low level

[Bryan Gin-ge Chen]

Also, you should be getting those from pushes, not pulls...

[Filippo A. E. Nuccio]

Bryan Gin-ge Chen said:

You can turn those notifications off from your GitHub settings.

Well, but I am wondering whether this is a signal of an issue

[Filippo A. E. Nuccio]

Bryan Gin-ge Chen said:

Also, you should be getting those from pushes, not pulls...

You're right, my mistake .

[Bryan Gin-ge Chen]

Well, the runs are failing because the code that you're pushing has errors in the Lean or some linting issues. It's usually fine.

[Filippo A. E. Nuccio]

Kevin Lacker said:

try running leanproject get-cache before building

Ok, now I could download the cache. And I am going to rebuild.

[Filippo A. E. Nuccio]

Nope, the terminal window says > lean --make src, the fan is taking off and a minute has passed...

[Filippo A. E. Nuccio]

(and it looks very much as before)

[Bryan Gin-ge Chen]

Here's the log for the build triggered by your most recent commit: https://github.com/leanprover-community/mathlib/runs/1261674429

[Bryan Gin-ge Chen]

You can see that the build hits an error on src/algebra/direct_limit.lean.

[Bryan Gin-ge Chen]

If that file isn't fixed, then you won't get oleans for anything "downstream".

[Filippo A. E. Nuccio]

I see-but I have never touched that file myself. Can't I just copy the version in master and hope it helps?

[Filippo A. E. Nuccio]

(well, provided my pc won't explose in the coming minutes, which seems like the next probable event)

[Kevin Lacker]

your pc is fine, you'll have a mildly elevated risk of hard drive failures if it keeps running this way for the next 3 months straight ;-)

[Kevin Lacker]

even if you never touched that file, you must be causing the build breakage somehow, since it's working in master

[Bryan Gin-ge Chen]

Filippo A. E. Nuccio said:

I see-but I have never touched that file myself. Can't I just copy the version in master and hope it helps?

This is unlikely to fix things.

I think @Anne Baanen can probably provide the best advice here.

[Filippo A. E. Nuccio]

I asked them a couple of times, but they don't seem to experience the same issue.

[Bryan Gin-ge Chen]

If it were me, I would git merge master and then try to fix all the conflicts and errors.

[Bryan Gin-ge Chen]

But that looks to be difficult at this point.

[Kevin Lacker]

are you working on your own branch, or are you sharing a branch with a bunch of other people, and you all kind of simultaneously check in code without being totally sure it works?

[Filippo A. E. Nuccio]

Kevin Lacker said:

even if you never touched that file, you must be causing the build breakage somehow, since it's working in master

I agree, but I have no idea on how to figure where the breakage takes place. Expecially because I did the leanproject build this afternoon, it took a hour or so; and after ten minutes of work on the newly rebuild library, I went back where I was

[Filippo A. E. Nuccio]

Well, technically we are three people working on this, but the other two members haven't touched the file in the last 3 weeks or so.

[Bryan Gin-ge Chen]

When you run leanproject build, you should pay attention to the output. If the word error shows up anywhere then things are broken.

[Filippo A. E. Nuccio]

And what do I do in that case?

[Bryan Gin-ge Chen]

You will have to fix the error or get someone to fix it for you.

[Kevin Lacker]

it looks like both you and Vierkantor have checked into the branch recently

[Kevin Lacker]

you can't look at just a single file - it's possible for a change in one file to break something in another file

[Filippo A. E. Nuccio]

Well, if the other file is downstream wrt mine, right?

[Kevin Lacker]

look at https://github.com/leanprover-community/mathlib/compare/Vierkantor-dedekind-domain

[Kevin Lacker]

it was passing checks as of commit https://github.com/leanprover-community/mathlib/commit/8c94fef07967472c2f839f4333f479888196efdb

[Kevin Lacker]

and then continuous integration broke here: https://github.com/leanprover-community/mathlib/commit/8bd048dc7a42350246468e323e4609c6bf1a2d31

[Kevin Lacker]

it looks like you did a merge which failed

[Kevin Lacker]

6 hours ago, you did a merge which had "313 changed files with 13,112 additions and 4,549 deletions"

[Kevin Lacker]

my guess is that one of those 313 files you changed had a problem

[Filippo A. E. Nuccio]

But how is it possible that I changed 313 files?

[Filippo A. E. Nuccio]

(let alone the 13,112 additions)?

[Kevin Lacker]

take a look, the commit where you did it is right here: https://github.com/leanprover-community/mathlib/commit/8bd048dc7a42350246468e323e4609c6bf1a2d31

[Kevin Lacker]

it looks like a massive merge, maybe you ran a huge git merge command without realizing it was a huge git merge command?

[Filippo A. E. Nuccio]

I am looking at that commit and am shocked...

[Filippo A. E. Nuccio]

I don't think I merged anything: I opened git, checked with git status that I was up to date and opened VLCode

[Filippo A. E. Nuccio]

worked a bit, then commit+pushed.

[Scott Morrison]

It could just be that you merged master at that point.

[Kevin Lacker]

git is kind of like a swiss army knife where one of the tools is a grenade. if you just kinda type one command wrong it can screw a lot of stuff up

[Filippo A. E. Nuccio]

but I never type commands on git. I work directly and only in VSCode

[Kevin Lacker]

shrug

[Filippo A. E. Nuccio]

For instance, it seems that I touched upon src/algebra/char_zero.lean

[Scott Morrison]

How do you merge master into your working branch, then?

[Scott Morrison]

Obviously the changes in that massive commit are changes other people have been making to master.

[Kevin Lacker]

you probably clicked "ok" to something in vscode that was actually a bad idea to click ok on

[Scott Morrison]

It can't be anything other than merging master in your branch.

[Kevin Lacker]

at any rate, what you want to do here is three steps

[Filippo A. E. Nuccio]

This is something @Anne Baanen does, normally. I usually only work in my local copy of their branch

[Scott Morrison]

On the other hand, merging master is something you have to do at some point.

[Kevin Lacker]

first, you made some changes after that massive merge. in this commit: https://github.com/leanprover-community/mathlib/commit/53a347b5d8c50f7b6d99fd94e2bb192b4688782e

[Kevin Lacker]

grab those changes and store them locally somehow. i would like, cut and paste them into a text file or something naive

[Kevin Lacker]

second, roll back your branch to before the merge broke everything

[Kevin Lacker]

probably google for some page of git commands, i never remember how to do this stuff

[Kevin Lacker]

third, reapply your changes that you intended to make, without doing that huge merge

[Filippo A. E. Nuccio]

Thanks, I will do this. But I'd like to undestand where this came from. I haven't typed merge a single time today

[Filippo A. E. Nuccio]

And I have been fighting against these issue since June or something

[Kevin Lacker]

there are several layers to this answer

[Kevin Lacker]

the most superficial answer is that it probably came from vscode, because most people set up vscode to interact with git. maybe you accidentally clicked some icon that does something

[Scott Morrison]

Do you ever run leanproject up?

[Filippo A. E. Nuccio]

Yes---I had been told it is more or less equivalent to get-cache

[Kevin Lacker]

the second level of answer is that the more you work against some branch that is super diverged from master, the more of these problems you will have. so you can avoid trouble by staying closer to master

[Filippo A. E. Nuccio]

Well, but if @Anne Baanen merged yesterday the master with their branch, and I pulled right before starting to work, I was pretty close , no?

[Filippo A. E. Nuccio]

AHAH: In the meanwhile leanproject build has finished with tons and tons of errors

[Kevin Lacker]

both of you are super far away from master, this separate branch has been open since August 4

[Kevin Lacker]

were you getting a bunch of error emails from continuous integration that you were ignoring?

[Filippo A. E. Nuccio]

Yes - very bad idea, I suppose.

[Kevin Lacker]

the thing to do when you get one is to look at the CI error - a page like this one: https://github.com/leanprover-community/mathlib/runs/1261674429

[Kevin Lacker]

if it seems like it's your fault, fix it. if it doesn't seem like it's your fault, look at the commit history. it's linked from that page if you click on the branch name. a page like this one: https://github.com/leanprover-community/mathlib/compare/Vierkantor-dedekind-domain

[Kevin Lacker]

the little X's on the right show you when the build was OK and when the build was broken

[Kevin Lacker]

in this case, you can see that there was an ok build earlier today, and then the first of the most recent block of X's is the commit you should be suspicious of

[Filippo A. E. Nuccio]

and when you say "it's your fault" do you mean that there is a non-compiling file?

[Kevin Lacker]

when I checked that commit, I saw that 1. you were the author and 2. it modified 300 files, which made me think aha looks like an accidental huge merge

[Kevin Lacker]

I mean that you committed the change that broke the build

[Kevin Lacker]

it might not be your fault if like, maybe there's something that breaks randomly once every 20 runs. then the test is at fault

[Kevin Lacker]

if you suspect something like that, have the CI system rerun the build

[Filippo A. E. Nuccio]

namely? I mean, it will complain and won't build, no?

[Kevin Lacker]

let's say the error is like, "error for free_comm_ring.lift, failed to synthesize type class instance". that sounds like your fault. but if the error is like, "error, hard drive failure detected, system rebooting." that doesn't sound like your fault.

[Filippo A. E. Nuccio]

yet I believe there must be some problem with my VSCode, or something. I have checkout to master, and again VSCode has been compiling for 5 minutes

[Filippo A. E. Nuccio]

although I have simply get-cache and then opened VSCode, without typing a single character

[Bryan Gin-ge Chen]

If you only git checkout, you don't have the corresponding olean files. So you'll need to build those locally or get them using leanproject get-cache..

[Filippo A. E. Nuccio]

so I did: checkout, then get-cache, then opened VSCode. I went to a file (without editing) to see if the Infoview would work, and here I am since 5 minutes.

[Kevin Lacker]

restart the lean server

[Filippo A. E. Nuccio]

done

[Filippo A. E. Nuccio]

orange bars...

[Kevin Lacker]

you're sure you're on master?

[Filippo A. E. Nuccio]

FAE@DESKTOP-MMB9C9K MINGW64 ~/Desktop/Lean/mathlib (Vierkantor-dedekind-domain)
$ git checkout master
Switched to branch 'master'
Your branch is up to date with 'origin/master'.

[Kevin Lacker]

git pull

[Filippo A. E. Nuccio]

done

[Kevin Lacker]

leanproject get-cache

[Filippo A. E. Nuccio]

going on...

[Filippo A. E. Nuccio]

done

[Kevin Lacker]

now see if things compile

[Filippo A. E. Nuccio]

now yes, everything nice and smooth

[Kevin Lacker]

great. now you can go fix your borked branch

[Filippo A. E. Nuccio]

I have removed my Git info from VSCode, so it can't do "too much".

[Filippo A. E. Nuccio]

Kevin Lacker said:

great. now you can go fix your borked branch

the steps you suggested before, right?

[Kevin Lacker]

yeah

[Filippo A. E. Nuccio]

so I need to merge master with the other branch - I suspect I will get some 400 errors, or so.

[Kevin Lacker]

mmm no you should not need to merge anything

[Kevin Lacker]

all you're doing is rolling back your branch

[Filippo A. E. Nuccio]

to https://github.com/leanprover-community/mathlib/commit/8c94fef07967472c2f839f4333f479888196efdb, for instance?

[Filippo A. E. Nuccio]

(the last commit this morning where everything was fine)

[Kevin Lacker]

yep

[Kevin Lacker]

some sort of git reset

[Filippo A. E. Nuccio]

OK, I am going to. Yet you agree that it is strange that there are so many red crosses, no? I mean, looking back at the history of the branch.

[Kevin Lacker]

well once you mentioned that you like to ignore emails about failing CI, it stopped surprising me that the history has a lot of failing points

[Filippo A. E. Nuccio]

It makes sense indeed.

[Filippo A. E. Nuccio]

I will try to go back to that commit and keep better track of what happens. Thanks so much for the help, in the meanwhile.

[Kevin Lacker]

no problem. good luck ;-)

[Filippo A. E. Nuccio]

@KevinLacker I am sorry, I am unable to get the things done, can I ask for more help?

[Heather Macbeth]

@Filippo A. E. Nuccio I don't know how to help you myself, but you can summon Kevin by writing @**name_here** rather than just @...

[Filippo A. E. Nuccio]

Hi Heather! Thanks, I have realised that after I typed, but also realised he's not connected any more. And am trying to figure out things without disturbing other people.

[Julian Berman]

I didn't follow the whole thread -- are you trying to figure out the git reset piece though or something bigger than that?

[Filippo A. E. Nuccio]

Thanks-I ended up resetting to a previous commit and now things are working.

[Julian Berman]

If it's just that I can likely help, it sounded like from the scrollback that you want git reset --hard somecommit, which is a slightly dangerous command to run in general but if we get somecommit right it's OK.

[Filippo A. E. Nuccio]

Thanks anyhow, but I grab the chance to ask why is it so dangerous

[Julian Berman]

Cool!

[Julian Berman]

Uh -- simply that it throws away commits -- normally the sequence of changes that are made stays "the same", but git reset --hard essentially moves you to a particular ref and doesn't preserve where you were

[Julian Berman]

(it will also, if you've pushed those commits elsewhere, now cause you to need to use git push --force, which will now make everyone else you may work with have some pain when they try to pull)

[Julian Berman]

So yeah in general you should think twice about using it but it sounded like it was what you needed here

[Filippo A. E. Nuccio]

I see, it certainly makes sense. I sometimes feel that git is a bit "overcautious" but I guess it's me.

[Kevin Buzzard]

(sorry, was sleeping). simp is not usually the culprit when you find yourself in the situation that every time you type something you have to wait for ten seconds. The more likely culprits are tidy and finish. Other possibilities: you are writing one 200 line proof instead of ten 20 line proofs, or maybe you are using a machine with less than 8 gigs of ram. In fact I sometimes struggle even with 8 gigs.

[Kevin Buzzard]

Note that this is an independent issue to things taking one hour to compile (which should never happen unless you're editing files deep in the system).

[Filippo A. E. Nuccio]

Thanks! I am really trying to figure out together with @Anne Baanen what is going on and I hope to have a more efficient system soon. BTW: I remember that during LFTCM2020 during a break-up room with @Sophie Morel you told us about "your favorite tactic" or something like this, which instead of inserting a have, replaces the current goal with something new, that you will later need to explain being equivalent to the old one. Do I remember correctly, what was this tactic?

[Anne Baanen]

Are you thinking of docs#tactic.interactive.convert?

[Filippo A. E. Nuccio]

Probably yes, thanks!