Build errors (sorry)

Stream: Polynomial Freiman-Ruzsa conjecture

[Terence Tao]

Just a note to apologize for creating a number of small build errors in the Lean code. An unintended consequence of accepting a PR to update Mathlib was that my local copy decided that it had to rebuild all of Mathlib, a process that is still ongoing right now. I thought somewhat naively that I could continue coding without the safety net of actually compiling the code but that was probably a mistake. Anyway, hopefully it will all be straightened out soon (and I will be significantly more wary of accepting major update PRs in the future). Thanks to everyone who already helped clean up the code!

[Shreyas Srinivas]

If it is rebuilding from scratch, you should probably run lake exe cache get

[Shreyas Srinivas]

It will significantly speed up the process

[Terence Tao]

Yeah, I tried that but I think I made the mistake of doing it while VScode was still running and it created some weird issues. I'm currently at 1283 of 1644 and am inclined to just try to wait it out

[Shreyas Srinivas]

Depending on your machine that is easily enough time to make some fresh coffee (in the range of 5-15 minutes)

[Mauricio Collares]

open ProbabilityTheory as well as replacing U : Ω → H by U : Ω → G in the two formulations of entropic_pfr fixes the build, but I don't know if isUniform H U μ is supposed to imply that the measure of the complement of H is zero. I can submit a PR if it is.

[Terence Tao]

Thanks, you are right, the intention is for U to range in G, and for isUniform to check that the complement of H is almost surely not attained.

It's somewhat eye-opening for me to realize how much I implicitly rely on the Lean infoview to check my work at every line; the moment that safety net is gone, all sorts of typos start creeping in...

[Yaël Dillies]

You can always close VS Code, open a terminal inside the project folder and run lake exe cache get there.

[Yaël Dillies]

What you encountered earlier is that the Lean extension builds the files and writes them to your disk, meaning that any attempt of getting cache will fail because the freshly downloaded cache will have been overwritten by the extension.

[Terence Tao]

Yeah, but it's a risk-reward calculation at this point. I'm at 1461/1644 right now and am wary that if I touch anything at this point I go back to 0/1644 (unlikely, I know, but it looks tantalisingly close right now).

[Mauricio Collares]

Yaël Dillies said:

What you encountered earlier is that the Lean extension builds the files and writes them to your disk, meaning that any attempt of getting cache will fail because the freshly downloaded cache will have been overwritten by the extension.

That's what I thought as well, but wouldn't this only lead to 8 (or however many cores you have) rebuilt files, since the downloaded cache and the locally-generated file will be the same? Or does lake check all hashes before building all files instead of doing it on-demand?

[Mauricio Collares]

I understand it processes files "top-down" starting with Mathlib.lean and ends up building them bottom-up, but there still seems to be an opportunity for short-circuiting if the olean/hash is rechecked right before it actually gets built.

[Mauricio Collares]

I'll take the liberty of pinging @Mac Malone (sorry for subscribing you here!)

[Kevin Buzzard]

Terence Tao said:

Yeah, but it's a risk-reward calculation at this point. I'm at 1461/1644 right now and am wary that if I touch anything at this point I go back to 0/1644 (unlikely, I know, but it looks tantalisingly close right now).

You never have to compile mathlib (unless you're editing mathlib itself), so in some sense there's 0 risk in aborting any attempt to compile mathlib. However it can sometimes be an art to get cache to work -- right now cache is failing to download 9 files for some reason (the experts are working on it). Right now my strategy is: (1) exit VS Code and fire up a command line (2) lake exe cache get (3) lake build (which will fix the "9 files didn't work" issue) (4) safe to open VS Code again.

[Richard Copley]

If lake exe cache get downloads all the files but fails to unpack them because Lean is still running (as a server for the editor), I've sometimes needed lake exe cache unpack! to fix the resulting mess.

[Kevin Buzzard]

yeah, running lake exe cache get when there are some other Lean's running somewhere gives unpredictable results. Instead of closing VS Code I sometimes fire up a terminal and type killall lean and then lake exe cache get.

[Terence Tao]

Yay, it reached 1644/1644, and infoview is working again! I'll add the lake suggestions to the troubleshooting section of my phrasebook, though, for future use.

[Terence Tao]

Oh, wait. every lean file wants to rebuild mathlib? OK, now I'm going to try the lake cache thing

[Shreyas Srinivas]

Probably not necessary

[Shreyas Srinivas]

Now that you built it once, it will be quicker

[Terence Tao]

Hmm, lake build is actually building all of mathlib all over again, not just the 9 missing files. (I'm currently at 609/1946). A bit faster than before, though.

[Shreyas Srinivas]

It should be done by now. lake should just be looking for oleans + some other stuff and finding them at this point.

[Terence Tao]

It seems to want do redo everything.

image.png

[Terence Tao]

It is a strange feeling though to see multiple substantial PR contributions to the project occuring simultaneously right now while my own copy remains stalled. This project has really started taking off...

[Shreyas Srinivas]

Is the repository on github the latest version you are trying to build right now?

[Terence Tao]

I believe so (plus or minus an hour or so)

[Rémy Degenne]

What I do in those situations where the build is broken beyond my ability to fix it is delete the folder, clone again and lake exe cache get. Takes 2 minutes, does not require understanding lake, works every time. That's good only if you have no local changes you want to keep though.

[Shreyas Srinivas]

I just tried building it and it works for me.

[Terence Tao]

Yeah, I did that once before for the symmetric project (ironically, again because I was trying to update mathlib). I am close to taking that option right now, but I'll see if this most recent build fixes all issues first. I wonder if there should just be a big button in the VSCode version control to do precisely this (i.e., nuke everything, clone from master, and retrieve cache).

[Terence Tao]

Shreyas Srinivas said:

I just tried building it and it works for me.

Well, it's good to know the problem is localized to my copy at least. There were at least five different contributors to the project in the last few hours, so there doesn't seem to be any global issue.

[Terence Tao]

Rémy Degenne said:

What I do in those situations where the build is broken beyond my ability to fix it is delete the folder, clone again and lake exe cache get. Takes 2 minutes, does not require understanding lake, works every time. That's good only if you have no local changes you want to keep though.

Though in the current situation with 9 missing files, one may still have to run lake build? Not sure why it is deciding to build even the files that were successfully unpacked from cache though.

[Rémy Degenne]

Those 9 missing files don't cause a lot of building thankfully. If lake exe cache get was successful the build should be quick (either from lake build or from rebuilding the dependencies of a file of the project in vscode).

[Mauricio Collares]

Previously Lean wasn't fully killed when you closed VS Code and this led to problems when running lake exe cache get even on a terminal. Closing VS Code should be enough in the most recent version (which you just updated to) though.