Please pick the version you prefer for Coq 8.18 in Coq Platform 2023.10

[rtetley]

The Coq team released Coq 8.18.0 on September 7th, 2023.
The corresponding Coq Platform release 2023.10 should be released before November 30th, 2023.
It can be delayed in case of difficulties until January 15th, 2023, but this should be an exception.

This issue is to inform you that the opam package we are currently testing in Coq Platform CI works fine with Coq 8.18.0.

Coq Platform CI is currently testing opam package coq-libhyps.2.0.6
from official repository https://coq.inria.fr/opam/released/packages/coq-libhyps/coq-libhyps.2.0.6/opam.

In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.

In case you would prefer to see an updated or an older version in the upcoming Coq Platform 2023.10, please inform us as soon as possible and before October 31st, 2023!

The working branch of Coq Platform, can be found here main.
It contains package pick ~8.18+beta1 which already supports Coq version 8.18.0 and contains already working (possibly patched / commit pinned) Coq Platform packages.

In case you want to select a different version, 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#372

[rtetley]

Hey @Matafou, doing a round of reminders. What is the status on this ?

[Matafou]

Hi, thanks for the reminder. 2.0.6 is fine. What should I do to confirm?

[rtetley]

Just closing the issue is perfect ! :-) I'll do it in this instance !

[MSoegtropIMC]

@Matafou : unfortunately 2.0.6 has an issue: the demo.v file doesn't run through (it fails at especialize H3 at 1.) Can you please have a look?

I would btw. appreciate if the demo.v file - which we use for smoke testing - would be in your CI.

Can you please reopen this ticket (I can't since @rtetley created it).

[Matafou]

especialize is indeed broken. It looks like something became more restricted with evar environments in coq. I will investigate, meanwhile do you have an option? Like disabling this feature for a while.
Indeed having the demo.v file in ci would have been nice.

[MSoegtropIMC]

I am having a few other issues, which likely will take me until Tuesday to fix. If you can fix it until then, please just create a new tag.

Otherwise I can't say what is a good solution here. I would suggest that we disable it and do an update in an update release. I plan anyway to do another Coq Platform release in 4 weeks or so with additional packages. I would then document in the release notes that especialise is broken and planned to be fixed soon.

[Matafou]

The regression is due to a regression in specialize AFAIU. The recent reimplementation of specialize is much cleaner than before but it does not support evars in its args type. I am not sure to be able to fix it from the especialize ltac code. I may try to propose a fix to coq, but I first need to understand the new code.

[Matafou]

Reported the regression here: coq/coq#18332.

[MSoegtropIMC]

@Matafou : in this case, can you please create an updated demo.v file? Or should I just disable the smoke test for libhyps for now?

[Matafou]

Should we have a warning like "Warning LibHyps is currently partially incompatible with coq-8.18. See http://... .".

[MSoegtropIMC]

I would mention this in the Coq Platform release notes.

[Matafou]

• a PR is currently submitted to coq for fixing the problem.
• I don't see any way of a workaround until this PR is merged in coq
• It would be nice to warn people having libhyps to not upgrade to 8.18 yet if they use especialize (probably very few people anyways).
• Is there a recommended way to have a ci ?

[MSoegtropIMC]

Is there a recommended way to have a ci ?

Your yaml file looks fine at first glance. If you have issues getting it to work (I saw a few failures - one is because the opam file says you need Coq 8.17 and you have 8.18, others look like a manual cancel) please let me know.

[Matafou]

@MSoegtropIMC how much time do I have left to adapt please?

[MSoegtropIMC]

I am about to do the release builds - some final nit picking. I would say tomorrow early afternoon I do the release builds.

As far as I recall the conclusion was that for 8.18 we skip especialize and you provide an adjusted smoke test file.

[Matafou]

@MSoegtropIMC I unplugged especialize and make a release (libhyps-2.0.7). The tests are modified accordingly.
Can you make this release go into coq platform please?

[Matafou]

Actually I am on it.

[Matafou]

PR done: coq/opam#2859 . Sorry for being so late, I hoped for some time to fix it before the release, but this is more complex than anticipated.

[Matafou]

Something went wrong in the ci. Will try to check this quickly.

[MSoegtropIMC]

Luckily for you I am having some other problems, so it will likely be Monday.

[Matafou]

That is fortunate :-).

I don't understand the problem. It seems related to the yaml file for testing.

https://github.com/Matafou/LibHyps/actions/runs/7219147143/job/19671456084

Could it be that I need a call to coq_makefile before make? if yes then I guess I need to understand how the build target works...

[MSoegtropIMC]

I don't know much about the coq docker actions, but the command failing is:

opam install --confirm-level=unsafe-yes -j 2 . --deps-only

The '.' I guess means that opam is instructed to install from an opam file in the current folder. Your project doesn't have one.

Note that the opam files in a root folder are slightly different from usual opam files, they contain e.g. the version number (which is otherwise part of the path). See e.g.

https://github.com/ott-lang/ott/blob/master/ott.opam
vs
https://github.com/ocaml/opam-repository/blob/d62bc9e05ca1402c1ac40a707b0be53698e06ddf/packages/ott/ott.0.33/opam

Note that usually you name the local file just opam - that they are named differently in ott is because it has two opam files.

[Matafou]

I made another release which passes the tests: coq/opam#2861 . This one should be ok. New PR for opam coq archive: coq/opam#2861 .

Sorry for the noise...

[MSoegtropIMC]

Perfect, thanks!

And I have to say "sorry for the noise" - at second look your project already had a local opam file. Good that you could find the root cause. I will update right away.

[MSoegtropIMC]

I just did the update (there was some OS breakage on Monday which had to be rolled back before I can do the release).

@Matafou : can you please close this issue (I can't).

[Matafou]

thanks!