Please create a tag for Coq 8.15 in Coq Platform 2022.02
MSoegtropIMC opened this issue · 22 comments
The Coq team released Coq 8.15.0 on January 13, 2022.
The corresponding Coq Platform release 2022.02 should be released before February 28, 2022.
It can be delayed in case of difficulties until April 11, 2022, but this should be an exception.
This issue is to inform you that to our (possibly a few days old) best knoweldege the latest released version of your project (1.0+8.14) does not work with Coq 8.15.0.
We tried to remove version restrictions in opam files and possibly make or configure files, but this did not suffice.
Please note that in Coq Platform CI (unlike Coq CI) we test only released / tagged versions. Coq CI appears to test this project, but has some special handling for your project which makes it difficult to retrieve the commit it tests for your project.
Could you please create a tag and opam package, or communicate us any existing tag that works with Coq branch v8.15, preferably before February 14, 2022?
In case we might have to delay the Coq Platform release cause of issues with your project, we would prefer to be informed about the situation as early as possible.
In case the tag and opam package are available before January 25, 2022, it will be included in an early Coq Platform beta release of the for Coq 8.15.0.
The working branch of Coq Platform, which already supports Coq version 8.15.0, can be found here https://github.com/coq/platform/tree/main.
Please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.
In any case, Coq Platform won't be released before this issue is closed!
Thanks!
P.S.: this issue has been created automatically based on CI status.
CC: coq/platform#193
The tag for coq 8.15 is
https://github.com/coq-community/coq-dpdgraph/releases/tag/v1.0%2B8.15
The corresponding opam package is
coq-dpdgraph.1.0+8.15
now available in opam-coq-archive/released
Thanks, I updated Coq Platform!
@ybertot : there is one rather weird thing going on: the new source tar ball doesn't contain the "tests" folder, which results in issues with the smoke test.
The "tests" folder exists in:
but not in:
Did you do something on purpose which could have this effect?
Yes, I did it on purpose, I forgot we wanted the smoke test. I'll fix it after the CoqPL workshop, expect it for monday.
Would you mind using the auto generated github tar balls (which is quite common in opam)? I find it mildly confusing that a source tar ball doesn't match the git tag.
The link would then be (https://github.com/coq-community/coq-dpdgraph/archive/refs/tags/v1.0+8.15.tar.gz)
@MSoegtropIMC as discussed on Zulip, we can't use the GitHub tarball as long as autoconf is used. I hope to port the project to fully use Dune during the next Coq hackathon, which for this project would get rid of the need for a separate tarball.
@palmskog : I don't quite see why this would be. We have many packages which do call autoconf (or autoreconf) from opam. IMHO this is the cleanest solution.
@MSoegtropIMC autoconf is a really inconvenient build dependency for released packages (a system package not available on some systems by default). Therefore, nearly all Coq packages declare conf-autoconf both a dev and build dependency:
"conf-autoconf" {build & dev}
This means that, for example, in the released packages for coq-flocq and coq-interval, there is no dependency at all on autoconf. You can see for yourself that the flocq-3.4.3 tag in the Flocq repo and the tarball are not the same (the configure script is not present in the tag).
@palmskog is it okay if I just create a new tag exceptionally named v1.0+8.15.1 and an opam package coq-dpdgraph-1.0-8.15.1?
Or should it rather be named v1.0.1+8.15 with opam package coq-dpdgraph-1.0.1-8.15?
Note that I expect to continue with version coq-dpdgraph-1.0-8.16 afterwards.
The other possibility is just to rewrite version v1.0+8.15 completely? Would that be acceptable or preferred?
@ybertot the best solution is likely to "rewrite" (re-tag) the version v1.0+8.15. Then, we just edit the opam package in the archive with the new checksum.
But I don't understand why a changed version for 8.15 would be required. My commit fe4c05c only adjusted the opam package and CI in the repo, and those changes are irrelevant to anyone using the opam archive package. More generally, we are already using best practices with autoconf in the opam archive like "conf-autoconf" {build & dev} for coq-dpdgraph.
It is just that made the mistake of editing Makefile.in to stop including the test suite in the opam package, this one change has to be reverted. If anybody installed coq-dpdgraph since last friday, they have a slightly different installation of coq-dpdgraph, which is not able to perform any self testing.
It is a minor nuisance.
OK, then since there aren't a lot of people who have installed the 8.15 version yet, I think the best approach is delete the release and the tag on GitHub, then recreate the release with the exact same name for the tag, and add the new .tgz tarball again with the same name. If you flag up here when this is done I can adjust the archive opam package.
@palmskog : I am quite sure that Coq Platform drags in dependencies which anyway need autoconf - it is for sure installed. Also I am not aware of any systems where it would be in any way tricky to get autoconf. IMHO it is a standard dependency. I would prefer to have packages where the tar ball matches the tag and which call autoconf explicitly.
I had btw. my share of trouble maintaining packages which call autoconf only exceptionally and manually. Maybe @ybertot remembers the discussion round we had a few years back at one of the Coq workshops in Nice, where we tried to figure out how to call autoconf for some package where the knowledge on how to do this got lost (it boiled down to autoreconf -i -s or so). I prefer to have the opam package take in the tag and do whatever is required to get the binaries without any fancy manual secret sauce steps in between.
@MSoegtropIMC I agree that the autoconf approach can lead to confusion and maintenance issues. But I think it "works" from the perspective that end users only need to consume the tarball generated by make dist (without using autoconf).
Packages without fancy packaging can likely be ported to use "plain tags". But as Théo Zimmermann pointed out, Dune-based packages which leverage dune-release may rely on substitution and generating a custom tarball. I know Emilio uses dune-release for SerAPI, for example, so he regularly puts custom tarballs like this one in releases: https://github.com/ejgallego/coq-serapi/releases/download/8.15.0%2B0.15.0/coq-serapi-8.15.0.0.15.0.tbz
Well dune is a different story - I have to look into it.
For autoconf I still think there is no good reason for separating out the autoconf step - IMHO it has more disadvantages than advantages when using it with opam, since opam knows the prerequisites and installs them. And up to now I have not heard of issues with the opam conf-autoconf package.
What makes sense for users not using opam is a different story - it might indeed be better to run autoconf upfront. But my arguments where about opam. I prefer to have complete build instructions from git tag to binary in opam.
That makes sense. I will give it a serious thought before the next release. For this one, I only need to fix the lack of test suite, and I am practically finished doing (doing a few checks, and then a PR on opam-coq-archive).
@palmskog : I updated the v1.0+8.15 release with a new tarball. I also created a PR on opam-coq-archive for the update on the opam file, which did not change name.
@ybertot thanks, that looks good.
@MSoegtropIMC just to check, should we also enable the coq-dpdgraph test suite in the released opam package? Or is it enough that you can run the test suite "manually" using the contents of the tarball? If we want the former, we could just just add:
run-test: [make "test-suite"]
to the coq-dpdpgraph.1.0+8.15 opam package definition.
@palmskog : I must admit that running tests beyond the smoke test is a bit of a weak spot in Coq Platform as yet - it is infeasible to run in CI. In the future I will think about running the tests locally as an extra pre-release test, but right now I wouldn't use test facilities. Currently my assumption is that all packages are reasonably well tested in their own CI.
OK, then since we are now running the test suite in coq-dpdgraph CI, I guess nothing additional is needed in the package definition.
@MSoegtrop: opam coq archive should be good to go now: names are the same as before:
https://github.com/coq-community/coq-dpdgraph/releases/tag/v1.0%2B8.15
and the opam package is coq-dpdgraph.1.0+8.15
@ybertot : thanks! I will reenable the smoke test for coq-dpdgraph. Please leave this issue open - I will close it when done.