CI failure

Stream: mathlib4

[Ruben Van de Velde]

If you get a failure in Check {Mathlib, Tactic, Counterexamples, Archive}.lean actually caused by an error in validate lake-manifest.json inputRevs, please merge master

[Bryan Gin-ge Chen]

We sometimes make changes / fixes to CI which require essentially all open PRs to merge master to build properly (#mathlib4 > CI "lint style" failure @ 💬 was another recent case). I wonder if it'd be helpful to have an informational label like please-merge-master and some automation to apply it to all open (non-draft) PRs, possibly with some other conditions. Maybe it could be triggered by some keywords in the merged PR?

[Kim Morrison]

Sorry about this, I didn't anticipate it requiring everyone to merge master...

Even better than telling everyone they need to merge master would be doing it for them, perhaps.

[Yakov Pechersky]

In my organization's repos, we get a button on our PRs when the branch is out of sync with master -- we can merge master using one click on the github PR page. Would it be possible to configure mathlib repo to turn on this setting? It would allow contributors to merge master without having to start up a git client.

[Ruben Van de Velde]

Yeah, it should be. I think we turned it off because it was too enticing for people even if there was no need to merge?

[Jovan Gerbscheid]

Is there a downside to merging master?

[Bryan Gin-ge Chen]

I'd be happy to enable the button if someone tells me where to find it!

[Bryan Gin-ge Chen]

Kim Morrison said:

Even better than telling everyone they need to merge master would be doing it for them, perhaps.

I'd rather leave control over merging in the hands of contributors -- it's possible that they have some local commits / changes that would be annoying to fix if we automatically merged. Though I guess maybe we could build in a way for people to opt out?

[Yakov Pechersky]

https://docs.github.com/en/repositories/configuring-branches-and-merges-in-your-repository/configuring-pull-request-merges/managing-suggestions-to-update-pull-request-branches

[Yakov Pechersky]

Ruben Van de Velde said:

Yeah, it should be. I think we turned it off because it was too enticing for people even if there was no need to merge?

Perhaps we can revisit that now that we switched to fork based PRs?

[Bryan Gin-ge Chen]

Thanks, enabled!

[Ruben Van de Velde]

I'm fine with trying and seeing if we encounter any downsides

[Bernhard Reinke]

I just got a CI failure after merging master in the Check {Mathlib, Tactic, Counterexamples, Archive}.lean step, I got Please run 'lake exe mk_all' to regenerate the import all files as an error.

This was the job: https://github.com/leanprover-community/mathlib4/actions/runs/17909716613/job/50918196805

[Riccardo Brasca]

This is caused by proofwidget, I am afraid the only thing you can do is "ignore it" and it will be solved soon.

[Kenny Lau]

#27215 is also having the same problem (i just merged master).
job: https://github.com/leanprover-community/mathlib4/actions/runs/17910399957/job/50920432983?pr=27215

[Chris Birkbeck]

me too. I am also getting: Failed to fetch ProofWidgets cloud release: lake failed with error code 1. Is this related?

[Miyahara Kō]

#lean4 > lake exe cache get failed to get github releases

[Riccardo Brasca]

We are working on it

[Sebastian Ullrich]

This issue has now been resolved (edit: confirmation on mathlib CI pending). Users with checkouts that have already run into this issue will need to delete their .lake folder first (lake clean does not suffice in this case).

[Bernhard Reinke]

Thanks! I bumped #27672, it passes CI again

[Kenny Lau]

@Bryan Gin-ge Chen I support the please-merge-master idea; I think the maintainers should have a button that applies it to all open PR's, and that button should be pressed every time they confirmed that there was a change that breaks all PR's

[Kevin Buzzard]

Master currently has a red x. The error is in "get cache for mathlib" and it's

...
✔ [18/19] Built Cache.Requests:c.o (1.5s)
✔ [19/19] Built cache:exe (442ms)
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed

  0     0    0     0    0     0      0      0 --:--:-- --:--:-- --:--:--     0
  0     0    0     0    0     0      0      0 --:--:--  0:00:01 --:--:--     0
  0     0    0     0    0     0      0      0 --:--:--  0:00:02 --:--:--     0
  0     0    0     0    0     0      0      0 --:--:--  0:00:02 --:--:--     0

100 1125k  100 1125k    0     0   502k      0  0:00:02  0:00:02 --:--:--  502k

lake stdout:
error: build failed
lake stderr:
error: build failed
uncaught exception: Failed to fetch ProofWidgets cloud release: lake failed with error code 1
installing leantar 0.1.16
Fetching ProofWidgets cloud release...
Error: Process completed with exit code 1.

[Bryan Gin-ge Chen]

Temporary network issue perhaps? Let's see if it goes away on the next commit.

[Kevin Buzzard]

Indeed it did.

[Yaël Dillies]

The autolabel workflow seems to be using some now-deprecated function: https://github.com/leanprover-community/mathlib4/actions/runs/19886384018/job/56994423828?pr=32381

[Yaël Dillies]

#32384

[Yaël Dillies]

@Markus Himmel

[Markus Himmel]

I went over the other scripts in the folder; this is the only one with a deprecation warning.

[Yaël Dillies]

It's worrying that this sort of errors can slip up. Should we have a MathlibScripts library that imports those lean files?

[Markus Himmel]

Well, I'd like to merge the PR, but...
image.png
image.png

[Markus Himmel]

Yaël Dillies said:

It's worrying that this sort of errors can slip up. Should we have a MathlibScripts library that imports those lean files?

That probably wouldn't work because you would have multiple declarations called main, but running something like lake build autolabel cache check-yaml mk_all lint-style check_title_labels pole unused as part of CI could be a good idea.

[Michael Rothgang]

#32388 fixes the "autolabel files" step in CI.