Mathlib bump

Stream: Polynomial Freiman-Ruzsa conjecture

[Scott Morrison]

I reduced the changes to the lake-manifest.json in https://github.com/teorth/pfr/pull/129/files (no functional change from my original PR, just making sure json blocks aren't unnecessarily reordered).

It compiles fine with lake build. Is there anything else to be concerned about? (If so, how about we check it in CI? :-)

[Terence Tao]

Scott Morrison said:

I reduced the changes to the lake-manifest.json in https://github.com/teorth/pfr/pull/129/files (no functional change from my original PR, just making sure json blocks aren't unnecessarily reordered).

It compiles fine with lake build. Is there anything else to be concerned about? (If so, how about we check it in CI? :-)

Hmm, as with previous bumps it caused my local version of Lean to recompile all of Mathlib, but that's fine. (I understand that I could presumably save the hour or two of building by doing lake cache get or something, but I'm not touching Lean any time soon, so I'm happy to just let it run. Still, I'm glad we waited until the project got over the finish line before approving the Mathlib rollover.)

[Yaël Dillies]

Now that we're reaching the "upstreaming" part of the project, please everyone expect mathlib bumps to become quite frequent!

[Yaël Dillies]

I would like to remind you that whenever you pull a bump PR to your local copy, you should run lake exe cache get right after. Importantly, do not click Rebuild imports or Refresh file dependencies or Restart file until you've run lake exe cache get.

[Kevin Buzzard]

So "before you upgrade, close VS Code, and don't open it again until after lake exe cache get". I usually type lake build as well before opening VS Code.

[Eric Wieser]

I don't think closing vscode is necessary any more

[Eric Wieser]

You just have to not click the popup that says "restart file" until you are actually ready to run Lean against your cache

[Adam Topaz]

crtl+shift+x is probably my most frequently used shortcut nowadays

[Kevin Buzzard]

For me closing and opening VS Code is cheap. I do it every time I fiddle on command line. Looking forward to a world where I never have to touch command line...

[Eric Rodriguez]

Developer: reload window is closing vscode but faster :)

[Eric Wieser]

Not clicking "restart file" is (in this case) "Developer: reload window" but faster :)

[Scott Morrison]

@Kevin Buzzard, what are the major things you're still doing on the command line?

• Restart file (via ctrl-shift-x) deals with out of date imports
• Under the \forall menu, selecting "Project Actions" then "Fetch Mathlib Build Cache" achieves the same as lake exe cache get
• "Developer: reload window" resolves many "how did I get into this weird state" problems.

If you're keen on a future of not needing the command line, I'd recommend you try using these as much as possible, and report back where the pain points are, or conditions when you still need the command line.

[Scott Morrison]

(this is saying the command-line-free future might already be here... in my demo talk on tuesday I installed Lean during the talk, and didn't touch a command line.)

[Yaël Dillies]

Heads up that I just bumped mathlib an hour ago.

[Yaël Dillies]

And bumped again just now.

[Terence Tao]

Yaël Dillies said:

And bumped again just now.

Just a headsup: as part of the entropy refactoring I've had to add lemmas to PFR/Mathlib/MeasureTheory/Integral/Bochner.lean , PFR/Mathlib/MeasureTheory/Integral/Lebesgue.lean ,
PFR/Mathlib/MeasureTheory/Measure/Dirac.lean , PFR/Mathlib/MeasureTheory/Measure/NullMeasurable.lean , and PFR/Mathlib/Probability/Kernel/Disintegration.lean (mostly along the lines of replacing finiteness hypotheses with countability hypotheses).

[Terence Tao]

Oof, I just discovered that updating Mathlib at the main branch causes other branches to want to update too. Now Lean is rebuilding Mathlib in the entropy refactoring branch, I hope this doesn't break too many more things

[Eric Wieser]

If you switch branch between different mathlib versions, you need to run lake exe cache get again

[Eric Wieser]

(it should use an offline cache if you were previously working on that version, but you still have to tell it to copy the files from the cache)

[Terence Tao]

Is there a way to merge changes in the main branch with changes in a refactoring branch without pushing those changes back into the main branch?

[Eric Wieser]

From the refactor branch, you can git merge the_main_branch

[Eric Wieser]

(which may be either main or master for your project, I don't know which)

[Terence Tao]

The refactor branch is currently building Mathlib files (554/1698 so far). Would it be safe to cancel this, close VSCode, run lake exe cache get and git merge master, and reopen VSCode?

[Yaël Dillies]

Yes, absolutely.

[Yaël Dillies]

Except you should git merge master then run lake exe cache get.

[Terence Tao]

Also: if I have checked out the refactor branch in VScode and then close VScode and open up a separate command line, will git still know that I am in that branch?

[Eric Wieser]

The knowledge about which branch you are in is stored in the filesystem (in the .git folder)

[Terence Tao]

ok. Trying it now :fingers_crossed:

[Terence Tao]

Oh crap there are merge conflicts

[Yaël Dillies]

Sorry :frown:

[Mauricio Collares]

git push will still sync your most recent commits (pre merge) with GitHub in case you haven't done so already

[Mauricio Collares]

Seems like the newest commit is quite recent, though

[Terence Tao]

Ugh Measure.lean is going to be a mess for a while now

[Mauricio Collares]

You can also git merge --abort if you'd rather undo it all and deal with it later

[Mauricio Collares]

(you'll lose any merging work you might have done, though)

[Terence Tao]

Actually it only created three errors in the file, hopefully I can fix them all manually.

[Terence Tao]

I was expecting an ocean of red

[Terence Tao]

Have to attend to other things right now, but hopefully this was only a speed bump.

[Terence Tao]

OK Measure.lean is repaired. Refactoring is back on track!

[Yaël Dillies]

Bumped again!