Stream: Coq devs & plugin devs

Topic: Coq org unused repos


view this post on Zulip Karl Palmskog (Nov 21 2022 at 08:54):

Isn't it time to archive these repos on GitHub? Untouched for years.

view this post on Zulip Michael Soegtrop (Nov 21 2022 at 09:30):

coq/prerequisites is actually in use by Coq Platform.

view this post on Zulip Michael Soegtrop (Nov 21 2022 at 09:30):

See https://github.com/coq/platform/blob/bb768b8431c0fd47a5f10b46cebce0105fd3fe4a/windows/create_installer_windows.sh#L406

view this post on Zulip Michael Soegtrop (Nov 21 2022 at 09:32):

The idea was to put files there which are unreliable to download in CI or vanish randomly e.g. when new versions are published. The selection of files change only rarely, though.

view this post on Zulip Michael Soegtrop (Nov 21 2022 at 09:34):

It is of cause a bit of an abuse to use only the releases section of a repo.

view this post on Zulip Karl Palmskog (Nov 21 2022 at 09:34):

seems a bit weird to use repo just for this file, couldn't this be hosted in the platform repo, e.g., as here: https://github.com/math-comp/math-comp/releases/tag/archive

view this post on Zulip Michael Soegtrop (Nov 21 2022 at 09:41):

Possibly. It was decided to do it this way because it would confuse Coq Platform users to see this file there. In Coq Platform Releases there should be Coq Platform releases and not NSIS releases. In the mathcomp cases you linked there are old mathcomp releases and not arbitrary stuff.

This has been discussed to quite some length and this was the solution we concluded on - afair @Théo Zimmermann suggested it back then.

We expected more activity there, though. We have been lucky with CI download stability in the last year.

view this post on Zulip Michael Soegtrop (Nov 21 2022 at 09:43):

Also it is expected that in the long run we will need more tags there, so this would mess up the tag view of Coq Platform.

view this post on Zulip Théo Zimmermann (Nov 21 2022 at 09:44):

Regarding https://github.com/coq/ltac2, it used to be archived at some point I think. I don't know / recall what happened for this not to be the case today. We can re-archive it.


Last updated: Feb 06 2023 at 20:02 UTC