The Windows CI is currently failing cause of the unavailability of (https://download.gnome.org/sources/gtksourceview/3.24/gtksourceview-3.24.11.tar.xz) - it is redirected to some mirror which is not there.
This brings me back to the discussion if Coq CI should have its own mirror for CI vital stuff. Does INRIA have facilities for this?
I don't know of anything in place already, but we could certainly build something.
Can you please investigate the possibilities?
I think another thing which would be needed for that is support in opam to redirect URLs- I don' think we want INRIA URLs in public opam packages and we don't want Coq specific opam packages for generic system stuff either.
I don't think redirecting URLs is needed. Just set up an Opam mirror and execute opam admin cache
.
@Guillaume Melquiond : just to make sure I understand right: one would call opam admin cache
on some machine, replicate the resulting cache to some server and tell the CI opam to fetch sources from this server?
Yes and no. You might just as well call opam admin cache
on the server. I don't see any reason to run the command on a separate computer.
Of cause this assumes you can run anything on the file server, which might not be the case (say you use an Amazon AWS or file server).
Note that we do have servers that we control fully.
So this shouldn't be an issue if we want to use them for this purpose.
Otherwise, another solution is to set up a cache in GitHub Actions.
The more one can do with a server, the harder it is to make secure, but obviously both variants are an option.
I also thought about a cache with a GitHub action, but I think for long term reliably we need a server we control anyway.
Last updated: Dec 07 2023 at 17:01 UTC