MetaCoq 1.0 for Coq 8.16

[mattam82]

ci-skip: coq-metacoq-erasure.1.0+8.16 coq-metacoq-pcuic.1.0+8.16 coq-metacoq-safechecker.1.0+8.16 coq-metacoq-template.1.0+8.16 coq-metacoq-translations.1.0+8.16

[mattam82]

@gares I have a strange behavior where the last package in the skip list is not ignored for some reason (the translations one) https://gitlab.com/coq/opam-coq-archive/-/jobs/2673704389
Looking at the script it's not obvious what is wrong.

[yforster]

Sorry for being late about this, but I think we should not remove the Equations version. This would mean that future Equations versions commit to still work with this package here, and from experience in the past this was usually not the case.

[palmskog]

@yforster but can't we let the opam bench detect this? Recall that we are continuously testing existing packages with latest versions of Coq and their dependencies, and then we change package definitions if something errors out.

[silene]

Looking at the script it's not obvious what is wrong.

You (or Github) have put a \r at the end of your line, which confuses the script.

[yforster]

@yforster but can't we let the opam bench detect this? Recall that we are continuously testing existing packages with latest versions of Coq and their dependencies, and then we change package definitions if something errors out.

I don't understand the opam bench well enough to answer this myself: If @mattam82 releases an Equations beta in extra-dev, does the opam bench catch that now the MetaCoq package in released is broken?

[mattam82]

@silene thanks!

[palmskog]

I don't understand the opam bench well enough to answer this myself: If @mattam82 releases an Equations beta in extra-dev, does the opam bench catch that now the MetaCoq package in released is broken?

released and extra-dev is tested separately. So the opam bench runner for extra-dev can catch problems with Equations+MetaCoq in extra-dev, but not the combination of released and extra-dev. But isn't the focus here on released?

[yforster]

My focus is on which questions will turn up in Zulip in the end :) If I have both released and extra-dev enabled (that's a usual situation for users I think) and do opam update, I can get into a state where the MetaCoq package is not installable anymore, right?

[palmskog]

Based on my experience, having both extra-dev and released activated is something almost exclusive to Coq devs and advanced users. And if they are that advanced, they should be able to report problems to archive maintainers. I think there are several installation quirks right now with extra-dev itself. So my recommendations are targeted towards giving released-only users a good experience. For example, if there is some minor release of Equations that gets into the next Coq Platform, MetaCoq will not work there unless the Equations bound is loosened.

[mattam82]

This finally works. I had to disable the with-test targets as we did not test them in our CI and they were utterly broken (just the Makefile stuff is broken in the opam setting, the files build fine). Fixed by MetaCoq/metacoq#730

[mattam82]

@yforster I think it's fine to loosen the equations bound for now, and get reports that things are not co-installable later. I don't release new equations versions that often, and usually we see breakage already in Coq's CI.

[mattam82]

We can put back the with-test targets with the next release, so from my side @palmskog this is ready to go.