Stream: Coq devs & plugin devs

Topic: Windows CI failure cause of gnome mirror unavailable

view this post on Zulip Michael Soegtrop (Jun 18 2021 at 10:44):

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?

view this post on Zulip Maxime Dénès (Jun 18 2021 at 11:05):

I don't know of anything in place already, but we could certainly build something.

view this post on Zulip Michael Soegtrop (Jun 18 2021 at 12:15):

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.

view this post on Zulip Guillaume Melquiond (Jun 18 2021 at 12:28):

I don't think redirecting URLs is needed. Just set up an Opam mirror and execute opam admin cache.

view this post on Zulip Michael Soegtrop (Jun 18 2021 at 14:21):

@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?

view this post on Zulip Guillaume Melquiond (Jun 18 2021 at 14:27):

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.

view this post on Zulip Michael Soegtrop (Jun 18 2021 at 15:26):

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).

view this post on Zulip Théo Zimmermann (Jun 18 2021 at 15:40):

Note that we do have servers that we control fully.

view this post on Zulip Théo Zimmermann (Jun 18 2021 at 15:40):

So this shouldn't be an issue if we want to use them for this purpose.

view this post on Zulip Théo Zimmermann (Jun 18 2021 at 15:40):

Otherwise, another solution is to set up a cache in GitHub Actions.

view this post on Zulip Michael Soegtrop (Jun 18 2021 at 15:57):

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: Jun 10 2023 at 06:31 UTC