Karl Palmskog (Nov 21 2022 at 08:54): Karl Palmskog (Nov 21 2022 at 08:54):Isn't it time to archive these repos on GitHub? Untouched for years.
Michael Soegtrop (Nov 21 2022 at 09:30):coq/prerequisites is actually in use by Coq Platform.
Michael Soegtrop (Nov 21 2022 at 09:30): 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.
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.
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
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.
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.
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: Dec 06 2023 at 13:01 UTC