Zulip Chat Archive

Stream: mathlib4

Topic: bump to 2023-07-15

Scott Morrison (Jul 20 2023 at 07:24):

@Wojciech Nawrocki, the latest Mathlib bump PR is working except for the CommDiag test of ProofWidgets.

Would you be able to look at #5992?

Scott Morrison (Jul 20 2023 at 07:27):

test/CommDiag.lean:1:0: error: object file
'./lake-packages/proofwidgets/build/lib/ProofWidgets/Component/GoalTypePanel.olean'
of module ProofWidgets.Component.GoalTypePanel does not exist

Scott Morrison (Jul 20 2023 at 07:29):

The test is working fine from VSCode; the failure seems to just be in CI.

Wojciech Nawrocki (Jul 20 2023 at 16:56):

Pushed a potential fix.

Scott Morrison (Jul 20 2023 at 23:00):

Excellent, thanks, I can take it from there.

Notification Bot (Jul 21 2023 at 17:11):

Wojciech Nawrocki has marked this topic as resolved.

Notification Bot (Jul 22 2023 at 07:29):

Scott Morrison has marked this topic as unresolved.

Scott Morrison (Jul 22 2023 at 07:30):

This has been marked as resolved (never really useful), but still isn't merged! :-) If someone could review this that would be great. Staying up to date with Lean saves lots of hassle.

Eric Wieser (Jul 27 2023 at 21:35):

http://speedcenter.informatik.kit.edu/mathlib4/run-detail/1fa02e6d-71e6-4183-bded-91b8488955bd suggests that this has had a significant performance loss on some files

Scott Morrison (Jul 28 2023 at 00:13):

We really need to be doing the bumps constantly, so we can more easily pinpoint what causes a regression like this. Having a bump PR take weeks to be merged is not so great.

Eric Wieser (Jul 28 2023 at 00:15):

One way to do that would be to bump by smaller amounts each time: for instance, bumping to the version just before a major Std/mathlib interface refactor (which should be a trivial merge), then bumping for the refactor alone (in this case the Fin stuff)

Scott Morrison (Jul 28 2023 at 00:45):

The constraint for bumping by smaller amount is how long review is taking. The last bump PR took 8 days to merge.

Scott Morrison (Jul 28 2023 at 00:46):

#6196 bumps to 2023-07-19, which is easy because that's what Std is at.

Scott Morrison (Jul 28 2023 at 00:56):

std4#201 is the no-op bump of Std to 2023-07-24. Past that requires some changes.

Scott Morrison (Jul 28 2023 at 01:55):

std4#202 then bumps to 2023-07-25, which requires some changes to rewrites because of lean4#2317.

Last updated: Dec 20 2023 at 11:08 UTC