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.

[David Loeffler]

CI seems to be repeatedly failing at "lint style" (the last 8 staging runs all failed). Here's a sample of the output:

info: downloading https://releases.lean-lang.org/lean4/v4.27.0-rc1/lean-4.27.0-rc1-linux.tar.zst
Error(Download(Msg("error during download")), State { next_error: Some(Error { description: "SSL peer certificate or SSH remote key was not OK", code: 60, extra: None }), backtrace: InternalBacktrace { backtrace: None } })
error: could not download file from 'https://releases.lean-lang.org/lean4/v4.27.0-rc1/lean-4.27.0-rc1-linux.tar.zst' to '/home/runner/.elan/tmp/awfx0jnquyemiec9_file'
info: caused by: error during download
info: caused by: [60] SSL peer certificate or SSH remote key was not OK
Error: Process completed with exit code 1.

[David Loeffler]

Seems to be affecting both "staging" runs and normal branch CI runs.

[Sebastian Ullrich]

Seems to be working again, we made a configuration change on that machine and it took some time to propagate

[Jovan Gerbscheid]

In #33760, the linting step in CI has been running for almost 2 hours. Is this happening more widely at the moment? It seems to block the runner from doing CI for other PRs.

[Bryan Gin-ge Chen]

Yes, unfortunately it has been happening widely and I don’t understand why yet. Hard to link from mobile but there’s a thread in this channel about it. It should be safe to cancel / restart the job.

[Damiano Testa]

#mathlib4 > slow linting step CI?

[Thomas Murrills]

Here’s one I personally haven’t seen before: a failure during lint-style > sudo apt get update saying the azure cli and ubuntu(?) repos are “no longer signed”.

E: Failed to fetch https://packages.microsoft.com/repos/azure-cli/dists/noble/InRelease  403  Forbidden [IP: 13.107.213.66 443]
E: The repository 'https://packages.microsoft.com/repos/azure-cli noble InRelease' is no longer signed.
E: Failed to fetch https://packages.microsoft.com/ubuntu/24.04/prod/dists/noble/InRelease  403  Forbidden [IP: 13.107.213.66 443]
E: The repository 'https://packages.microsoft.com/ubuntu/24.04/prod noble InRelease' is no longer signed.
Error: Process completed with exit code 100.

[Michael Stoll]

I just received a bunch of emails telling me that various CI steps (on #34330) were cancelled. It looks like no runner was available to carry them out for 15 minutes. (The build step did get picked up, though, but everything else looks like it was cancelled.)

[David Loeffler]

I'm seeing the same with #34402 – everything except the primary build step timing out for lack of a runner.

[Michael Stoll]

It may be the case that the build step runs on a different set of machines (Hoskinson) than everything else (github)?

[Jovan Gerbscheid]

CI in batteries is also not working.

[Jovan Gerbscheid]

#34685 also failed to be merged by bors, presumable because of the same issue.

[Sebastian Ullrich]

#rss > GitHub Status - Incident History

We continue to investigate failures impacting GitHub Actions hosted-runner jobs.

[Yongxi Lin (Aaron)]

The CI for #34890 fails at the Post-Build step. I am not sure how to fix this. May somebody take a look?

[Bryan Gin-ge Chen]

It looks like a temporary network issue with https://releases.lean-lang.org/. I restarted the job

[Andrew Yang]

CI seems to be giving lots of weird errors:

Error: fatal: unable to access 'https://github.com/leanprover-community/mathlib4/': The requested URL returned error: 500

See e.g. here

Is it related to #rss > GitHub Status - Incident History?

We are investigating reports of degraded performance for Pull Requests

[Yongxi Lin (Aaron)]

The CI for my PR #35431 fails with the error: failed to parse latest release tag. Does anybody know how I can resolve it?

[Kim Morrison]

Looks like this was a transient failure.