CI: fetch Iris and std++ from github mirrors - #22321
Merged
Merged
Conversation
coqbot-app
Bot
added
the
needs: full CI
SkySkimmer
reviewed
Jul 29, 2026
Contributor
|
Cc @4ever2 nixpkgs may need a similar update |
RalfJung
force-pushed
the
iris-stdpp-mirrors
branch
from
July 29, 2026 08:02
46f3edb to
1a622c0
Compare
Contributor
Author
|
@coqbot run full ci |
coqbot-app
Bot
removed
the
needs: full CI
RalfJung
force-pushed
the
iris-stdpp-mirrors
branch
from
July 29, 2026 18:20
1a622c0 to
dafd65a
Compare
coqbot-app
Bot
added
the
needs: full CI
Contributor
Author
|
There is now also a mirror for Iris-examples on Github so I updated the PR to also use that. I'll leave managing the CI to you as I don't fully understand how it is supposed to work. :) |
Contributor
|
@coqbot run full ci |
coqbot-app
Bot
removed
the
needs: full CI
Contributor
|
we also have Line 400 in 8641bb7 |
Contributor
Author
|
Yeah I know -- we don't have a mirror for that yet. We'll set one up eventually but we can merge this meanwhile to deal with the existing rate limiting errors you are seeing. |
Contributor
Author
|
Those errors don't look like they can be caused by this PR? |
SkySkimmer
approved these changes
Jul 29, 2026
Contributor
|
failures are also on master |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
MPI's gitlab server is buckling under the load of aggressive scrapers which are likely fueled by the global craze for LLMs. We had to install aggressive rate limiting.
So we set up a mirror on github to prevent Rocq CI from being caught up in this rate limiting.