prelude check fails when rebasing onto nightly-with-mathlib

Stream: lean4

[Thomas Murrills]

I'm just experimenting with a draft PR to try to fix a bug in lean4, and things work fine on master—but when I rebase onto nightly-with-mathlib to test, "Check for modules that should use prelude / check-prelude (pull_request) " fails (listing a bunch of files I haven't touched). Does anyone know what this means/how to fix it?

[Matthew Ballard]

lean#3374 and lean#3463 is what I noticed

[Thomas Murrills]

Ah, hmm. What's the best solution here? I imagine nightly-with-mathlib will catch up sooner or later, but it seems about a week behind...

[Matthew Ballard]

What is the reason you on nightly with mathlib to start?

[Matthew Ballard]

There is a clean up from zeta reduction changes in simp ongoing that has broken nightly for a bit

[Thomas Murrills]

I'm currently hitting ":exclamation: Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch", and I'd like to attempt Std/Mathlib CI.

[Matthew Ballard]

Yeah, I was just wondering if you really wanted std and mathlib. Since you do, I think you have to wait

[Thomas Murrills]

Hmm. I wonder if I could cherry-pick the result of lean#3463 into (onto?) my branch in the meantime.

[Matthew Ballard]

Or you could disable the CI temporarily :smiling_devil:

[Matthew Ballard]

But mathlib won’t build still

[Thomas Murrills]

Oh, earlier you meant that nightly-with-testing (I'm mixing my branches:nightly-with-mathlib) itself breaks mathlib?

[Matthew Ballard]

Yeah, sorry if that was unclear

[Matthew Ballard]

See the most recent CI run

[Thomas Murrills]

Ah gotcha, part of me was hoping you did literally mean (lean4) nightly :P

[Henrik Böving]

Thomas Murrills said:

I'm just experimenting with a draft PR to try to fix a bug in lean4, and things work fine on master—but when I rebase onto nightly-with-mathlib to test, "Check for modules that should use prelude / check-prelude (pull_request) " fails (listing a bunch of files I haven't touched). Does anyone know what this means/how to fix it?

https://lean-lang.org/lean4/doc/dev/index.html#prelude this is the reasoning