Michael Soegtrop (Jun 14 2022 at 09:10): Michael Soegtrop (Jun 14 2022 at 09:10):@Enrico Tassi : I have difficulties finding a version of elpi which compiles with 8.16+rc1 - which is a bit odd since it is in Coq CI. I tried the latest commits of master and coq-master, neither of which compile.
Enrico Tassi (Jun 14 2022 at 09:11):Weird, coq-master should. gimme a pointer to the error plz
Michael Soegtrop (Jun 14 2022 at 09:19):With commit 9df8ecfc3cb0fed219138892d1789ef08e825f12 I got:
# File "src/coq_elpi_vernacular.ml", line 29, characters 45-49:
# 29 | let hash = Digest.file (EP.resolve_file ~elpi ~unit:x ()) in
# ^^^^
# Error: The function applied to this argument has type
# ?cwd:string -> file:string -> string
# This argument cannot be applied with label ~elpi
# make[1]: *** [src/coq_elpi_vernacular.cmo] Error 2
# make: *** [build-core] Error 2
This should be coq-master - with master I got different errors (afair).
Enrico Tassi (Jun 14 2022 at 09:21):This is the wrong version of elpi, you should use 1.15.x
Enrico Tassi (Jun 14 2022 at 09:21):Anyway, I hope to make a release for 8.16 by the end of next week...
Michael Soegtrop (Jun 14 2022 at 09:21):Ah yes - silly mistake.
Karl Palmskog (Jun 14 2022 at 09:23):@Michael Soegtrop please don't select some arbitrary working SHA for aac-tactics even in a preview. Since we now have 8.16+rc1 on Nix, I will be able to test with that in CI and do a release by Thursday June 16 at the latest.
Michael Soegtrop (Jun 14 2022 at 09:24):And yes, I wonder what the best process is. In the past it wasn't like that that the majority of packages don't work. Usually I just had to patch the opam packages to allow the latest Coq.
With 8.16+rc1 this does not work for the majority of packages.
I wonder if I should wait 2 weeks and see what works then before I make a development release.
Michael Soegtrop (Jun 14 2022 at 09:25):@Karl Palmskog : yes, I figured that for 8.16+rc1 the strategy I followed for previews releases doesn't make a lot of sense.
Michael Soegtrop (Jun 14 2022 at 09:26):I guess I will wait until end of June, see what works then and make the preview release then.
Michael Soegtrop (Jun 14 2022 at 09:27):Which I guess also means that I should do a release for 8.15.2 now. (I was waiting here for the opam packages to become available in the opam MinGW repo, but I can add them to the local patch repo).
Karl Palmskog (Jun 14 2022 at 09:29):yes, I think it's better not to mix up bugfix releases and preview releases if previews can take time
Michael Soegtrop (Jun 14 2022 at 09:36):OK, so I will do a 2022.04.1 release asap (if Coq 8.15.2 is not yet in the MinGW opam repo, I will copy the opam files to the Coq Platform repo).
For 8.16 there is still plenty of time and no reason to hurry things. But it was interesting to see what works and what doesn't anyway - it is interesting for future release planning.
Théo Zimmermann (Jun 14 2022 at 09:45):Given that the preview release is being delayed, and now that Docker-Coq images and a Nix package for Coq 8.16+rc1 are available, I think it becomes worthwhile to open issues on maintainers' repo to let them know that a release is being prepared and that they get a say in which version is included.
Pierre Roux (Jun 14 2022 at 09:50):Note that we don't have Docker image for 8.16+rc1 yet (we just recovered dev recently, 8.16 is waiting for serapi IINM)
Michael Soegtrop (Jun 14 2022 at 09:50):@Théo Zimmermann : the (minor) issue with that is that in the past I included information about the status of the latest release of a package (it it works with just weakening version restrictions or not). In the current state for 8.16+rc1 this makes little sense, because important dependencies are missing.
IMHO it would make sense to wait 2 weeks and create more informative issues, but I am open to removing the status info and create the issues now.
Michael Soegtrop (Jun 14 2022 at 09:51):@Pierre Roux : what is your view on the timeline?
Pierre Roux (Jun 14 2022 at 09:52):Can't say, that's in the hands of @Emilio Jesús Gallego Arias and @Erik Martin-Dorel
Théo Zimmermann (Jun 14 2022 at 10:50):Oh right, I forgot about SerAPI. We should really consider not providing SerAPI in the rc images IMO.
Théo Zimmermann (Jun 14 2022 at 10:52):@Michael Soegtrop What would be interesting (but that would require refining the notification script) would be to only notify maintainers of packages for which a compatible release of a dependency is available. In fact, ideally (but that would require writing even more automation), a bot would post these issues progressively as release of dependencies become available.
Emilio Jesús Gallego Arias (Jun 14 2022 at 11:02):Sorry folks, I've been very busy, will take care of this ASAP
Emilio Jesús Gallego Arias (Jun 14 2022 at 11:05):I have a branch working already, just need to find time to push it
Michael Soegtrop (Jun 14 2022 at 11:16):@Théo Zimmermann : indeed it would be a very reasonable process to inform package maintainers as soon as (proper) releases for all dependencies are available - and in case this is not yet the case say 4 weeks before the release deadline inform them about this situation. I will create a script for that - at first for "supervised automated operation" and if this becomes stable, we can make a bot from it.
Any objections against this process?
Pierre Roux (Jun 14 2022 at 13:28):Théo Zimmermann said:
We should really consider not providing SerAPI in the rc images IMO.
@Erik Martin-Dorel would that be easy? (if yes, that could certainly be useful)
Emilio Jesús Gallego Arias (Jun 14 2022 at 14:38):The current setup is very painful tho
Emilio Jesús Gallego Arias (Jun 14 2022 at 14:38):I can't install coq-mathcomp in 8.16+rc1 for example
Emilio Jesús Gallego Arias (Jun 14 2022 at 14:38):I guess I don't know how to use the opam setup
Emilio Jesús Gallego Arias (Jun 14 2022 at 14:38):but it is really difficult to test a new release for the RC
Emilio Jesús Gallego Arias (Jun 14 2022 at 14:38):Unless of course I roll my own tooling
Théo Zimmermann (Jun 14 2022 at 15:05):This is a chicken and egg problem: tooling, such as Docker-Coq images, is needed for maintainers of packages, but SerAPI is needed to create the images.
Théo Zimmermann (Jun 14 2022 at 15:06):That's one more reason for not including SerAPI in the rc image (leaving more time to get a more stabilized ecosystem so that SerAPI can be properly tested).
Emilio Jesús Gallego Arias (Jun 14 2022 at 15:08):Turns out math-comp stable is really broken with 8.16
Matthieu Sozeau (Jun 14 2022 at 15:09):Théo Zimmermann said:
Oh right, I forgot about SerAPI. We should really consider not providing SerAPI in the rc images IMO.
Agreed with that, we should have the least dependencies possible in those images (or rather build fancier images by layers), so that developers can gradually update the packages. AFAIK, I don't need serapi to test equations on 8.16+rc1 but it's blocking me (i.e. I can't use the docker coq images).
Emilio Jesús Gallego Arias (Jun 14 2022 at 15:23):Ok, here is the branch
Emilio Jesús Gallego Arias (Jun 14 2022 at 15:23):https://github.com/ejgallego/coq-serapi/tree/v8.16
Emilio Jesús Gallego Arias (Jun 14 2022 at 15:23):I could test it locally, but indeed CI is hard due to math-comp not being compatible with 8.16 IIUC
Pierre Roux (Jun 14 2022 at 15:40):Emilio Jesús Gallego Arias said:
Turns out math-comp stable is really broken with 8.16
Yes, we need to do a release. Meanwhile, opam install coq-mathcomp.dev should work (after adding the extra-dev repo).
Emilio Jesús Gallego Arias (Jun 14 2022 at 17:35):Thanks @Pierre Roux , using the extra-dev repos helped, I will tag serapi
Emilio Jesús Gallego Arias (Jun 14 2022 at 17:37):https://github.com/ejgallego/coq-serapi/releases/tag/8.16%2Brc1%2B0.16.0
Erik Martin-Dorel (Jun 14 2022 at 19:11):Thanks a lot @Emilio Jesús Gallego Arias !
I'm going to open a PR to add the version you tagged in extra-dev.
BTW out of curiosity, what is the x-commit-hash: datum?
Erik Martin-Dorel (Jun 14 2022 at 19:20):Pierre Roux said:
Théo Zimmermann said:
We should really consider not providing SerAPI in the rc images IMO.
Erik Martin-Dorel would that be easy? (if yes, that could certainly be useful)
I wouldn't say it's easier or not. It's just a matter of policy, and of course we can change if the trade-off is better.
Actually the current choice has been motivated by the wish to "add coq-serapi in all docker-coq images… except for coqorg/coq:dev as coq-serapi wasn't/couldn't easily be part of Coq's CI".
So I don't object at all to the alternative choice of not adding coq-serapi in Coq 8.17+rc1, however don't you think it would just delay the same packaging issue, when coq-serapi should be added in 8.17.0 ? with less opportunities to reproduce issues and so on…
Erik Martin-Dorel (Jun 14 2022 at 19:22):But admittedly, it's true that coq-serapi's status is a bit different than e.g. coq-bignums, because it is first part of extra-dev, then released in the central opam-repository.
Anyway, this latter think does not really look like a drawback to me… and if a "release notify helper script" that @Michael Soegtrop suggests can be developed, it would be very great 👍👍 and maybe reduce the pressure at Coq 8.x+rc1 tagging time(?)
Erik Martin-Dorel (Jun 14 2022 at 19:28):Théo Zimmermann said:
This is a chicken and egg problem: tooling, such as Docker-Coq images, is needed for maintainers of packages, but SerAPI is needed to create the images.
Yes I see what you mean, but actually there's something that's easy to do given the currrent infrastucture (even more now since all docker-coq images are mono-switch), something what we already did sometimes at some coq beta releases… but not this time unfortunately (just because lack of "anticipated notifications" I guess). This idea is as follows:
Just after the alpha branch is created (say, v8.17), we can easily create a continuously updated docker-coq image, tagged coqorg/coq:8.17-alpha, that does not contain coq-serapi but allows coq devs and package maintainers to anticipate testing… (with less than 30' lag = the image compilation time, between a commit pushed in v8.17 and the image pushed to Docker Hub). WDYT?
Erik Martin-Dorel (Jun 14 2022 at 20:30):Erik Martin-Dorel said:
Thanks a lot Emilio Jesús Gallego Arias !
I'm going to open a PR to add the version you tagged in extra-dev.
BTW out of curiosity, what is the
x-commit-hash:datum?
Actually Karl has been faster than me ( https://github.com/coq/opam-coq-archive/pull/2200 ), thanks @Karl Palmskog !
Karl Palmskog (Jun 14 2022 at 21:02):I think an 8.17 alpha Docker image is a good idea (in fact we had this before for some versions)
Emilio Jesús Gallego Arias (Jun 14 2022 at 23:17):Indeed I wonder what is the best way to keep this up to date. For now we are using Coq's CI, but we could use Coq Universe maybe for 8.17. In a sense it has been discussed keeping the CI pinned as Coq Universe is
Emilio Jesús Gallego Arias (Jun 14 2022 at 23:17):for a long time, I dunno
Emilio Jesús Gallego Arias (Jun 14 2022 at 23:18):For me the first thing I'd like to have is better tooling for branching / pinning
Erik Martin-Dorel (Jun 14 2022 at 23:20):Just FYI, I've just merged the docker-keeper spec of the Docker-Coq image for V8.16+rc1:
https://github.com/coq-community/docker-coq/pull/48
The five corresponding images will be available in ~30' as soon as this pipeline completes:
https://gitlab.com/coq-community/docker-coq/-/pipelines/563927654
If need be, see the list of tags on Docker Hub (which is already up-to-date):
https://hub.docker.com/r/coqorg/coq#supported-tags
Erik Martin-Dorel (Jun 14 2022 at 23:21):@Emilio Jesús Gallego Arias What is Coq Universe BTW?
Erik Martin-Dorel (Jun 14 2022 at 23:32):Anyway, I agree with @Karl Palmskog viewpoint that we should focus on deploying coqorg/coq:8.17-alpha at the right time (which should avoid what Théo referred above to as "a chicken and egg problem").
Ideally, the 8.17 release manager should ping me as soon as the v8.17 branch is created so we look after this in due time with Théo (I just need for him to configure a gitlab webhook)
@Théo Zimmermann feel free to check this process item is documented somewhere, if you agree of course
Emilio Jesús Gallego Arias (Jun 15 2022 at 00:32):@Erik Martin-Dorel a experimental project where everything is composed and built with dune c.f. https://github.com/ejgallego/coq-universe (see stream for more info / discussion)
Karl Palmskog (Jun 15 2022 at 09:34):I like the Coq Universe, but I don't think we have a critical mass of projects that support Dune yet to allow it to be a practical recommended testing ground
Last updated: Jun 03 2023 at 05:01 UTC