Coq Release 8.17 · Coq devs & plugin devs

That's undefined. Just let me know which PRs you think should go in and are almost ready / undergoing review.

Emilio Jesús Gallego Arias (Nov 16 2022 at 19:36):

Olivier Laurent (Nov 16 2022 at 22:22):

I was thinking about removing some deprecated statements from stdlib (in the spirit of #14819, but stdlib only) but I will not be able to do it before early December. Is it reasonable to try something for 8.17?

Théo Zimmermann (Nov 17 2022 at 07:11):

If it requires overlays, then probably this will be too late. But is this an issue if this removal only lands in Coq 8.18?

Olivier Laurent (Nov 17 2022 at 07:29):

Not really, just that with the two-versions delay for deprecation, it makes things long for renaming operations for example (at least 4 versions). I will try to focus on such deprecations and see if they induce overlays. If it is OK with you I try to do it very early December and we see at this point if it could make it for 8.17 or not (8.18 should not be a big problem).

Emilio Jesús Gallego Arias (Nov 17 2022 at 20:11):

I've cleaned up my PR's milestones; there are two important ones I'd like to see in 8.17 (and IMHO ready, modulo review) , the rest are postponed.

Théo Zimmermann (Nov 18 2022 at 09:46):

What I meant to understand was: if this removal lands in Coq 8.17, will that unlock work in Coq 8.18 that would otherwise need to be postponed?

Olivier Laurent (Nov 18 2022 at 10:12):

I think we agree. Concretely I would say maybe no unlock for Coq 8.18 but possibly for Coq 8.19 (two-versions deprecation delay), and I will first focus on removals having such a possible impact then.

Théo Zimmermann (Nov 21 2022 at 16:45):

@Erik Martin-Dorel The v8.17 branch has been created. We should start working on making Docker-Coq images available.

Théo Zimmermann (Nov 21 2022 at 16:50):

It is a bit strange because currently we have a

https://gitlab.com/api/v4/projects/19687072/ref/master/trigger/pipeline?token=XXXX&variables[CRON_MODE]=rebuild-keyword&variables[ITEM]=dev

webhook set for push events to the master branch and a

https://gitlab.com/api/v4/projects/19687072/ref/master/trigger/pipeline?token=XXXX&variables[CRON_MODE]=rebuild-keyword&variables[ITEM]=8.13

webhook set for push events to the v8.13 branch. It looks like the latter is completely outdated. Should I replace it with the equivalent for v8.17?

Karl Palmskog (Nov 21 2022 at 16:53):

@Théo Zimmermann usually we start by creating the 8.17.dev opam package. But now there are split packages, right? So one needs to add coq-core.8.17.dev and coq-stdlib.8.17.dev, etc.

Théo Zimmermann (Nov 21 2022 at 17:00):

Théo Zimmermann (Nov 21 2022 at 17:01):

But I have some doubts that Docker-Coq actually uses the definition in the core-dev repository. IINM, it uses the opam definitions from the repo directly.

Karl Palmskog (Nov 21 2022 at 17:27):

Théo Zimmermann (Nov 21 2022 at 17:35):

Karl Palmskog (Nov 21 2022 at 17:48):

not sure, I guess Erik can/will comment. In any case, would be good to have core-dev opam packages for testing

Théo Zimmermann (Nov 21 2022 at 17:49):

Karl Palmskog (Nov 21 2022 at 17:50):

Erik Martin-Dorel (Nov 21 2022 at 21:24):

exactly. This latter trigger amounts to providing up-to-date alpha images (before the beta release), and it just happens we had only provided beta images directly for the past few releases.
So yes, just replace (v8.13, [ITEM]=8.13) with (v8.17, [ITEM]=8.17) for now, but later on (or now as well if you want), I'd ask you to add one such trigger for all (v8.8 ≤ v8.16) branches as well → see https://github.com/coq-community/docker-coq/issues/49

Théo Zimmermann (Nov 22 2022 at 10:31):

@Erik Martin-Dorel I've set the webhook for v8.17 for now. You didn't clarify if the Docker-Coq building process currently uses the opam definitions from the repo or from opam-coq-archive. The conclusion from the discussion you linked was that we should prefer the opam definition from opam-coq-archive for better maintainability. OTOH, for a new branch like v8.17, these definitions might not be available yet, so using the opam definition from the repo will allow creating Docker images earlier.

Théo Zimmermann (Nov 27 2022 at 17:03):

@Erik Martin-Dorel The webhook for v8.17 does not seem to be sufficient for the Docker-Coq images to build for this branch without any other action. This pipeline https://gitlab.com/coq-community/docker-coq/-/pipelines/705952743 was triggered from the v8.17 branch with ITEM=8.17 set and it didn't do anything new.

Erik Martin-Dorel (Nov 28 2022 at 02:25):

Yes @Théo Zimmermann I know, I need to uncomment/check/push the 8.17 config in docker-coq master.
Sorry, was swamped with exam prep.
I'll push this very soon (unless you open a PR faster!, targeting the images.yml file)

Karl Palmskog (Dec 01 2022 at 13:49):

@Théo Zimmermann has it been decided if 8.17.0 will be compatible with OCaml 5 or not? Or perhaps 8.17.1?

Karl Palmskog (Dec 01 2022 at 13:50):

(or I should say, if there is any chance of 8.17.0 or 8.17.1 being compatible with OCaml 5)

Théo Zimmermann (Dec 01 2022 at 15:45):

Guillaume Melquiond (Dec 01 2022 at 16:15):

For what is worth, I am able to compile the standard library with a Coq compiled with OCaml 5. (But I have not tried to run the testsuite nor any contribution.)

Gaëtan Gilbert (Dec 01 2022 at 16:18):

Guillaume Melquiond (Dec 01 2022 at 16:19):

It should rather say that it is an issue only for native_compute, which people do not mind disabling if the compiler is OCaml 5.

Matthieu Sozeau (Dec 02 2022 at 10:19):

Emilio Jesús Gallego Arias (Dec 06 2022 at 13:30):

#15494 was able to run the test-suite with trunk (now 5.0) a few times in the past, so at least we have that data point.

Théo Zimmermann (Dec 19 2022 at 15:30):

FWIW, I'm waiting for coq/coq#16997, coq/coq#16981, and a decision on what to do with coq/coq#16994 before preparing the changelog PR and tagging 8.17+rc1. AFAICT, the rest of the issues / PRs in the 8.17+rc1 milestone are non-blocking.

Emilio Jesús Gallego Arias (Dec 19 2022 at 16:02):

#16978 is IMO important too; I'll fix the logic leading to the performance regression, that shouldn't be hard; indeed gtk already has the get_iter_at_line_index to be able to compute char positions efficiently, it is just that the code we have now got extremely convoluted as it had to workaround Coq returning incorrect parsing locations.

Karl Palmskog (Dec 19 2022 at 16:03):

as usual, we need three things after the release of 8.17+rc1 to enable testing in CI:

Karl Palmskog (Dec 19 2022 at 16:08):

if bignums or serapi tags could even be done before rc1, that might speed things up.

Emilio Jesús Gallego Arias (Dec 19 2022 at 16:32):

Pierre Roux (Dec 19 2022 at 17:05):

Karl Palmskog (Dec 19 2022 at 17:39):

I think we should always use packages based on tags for testing release candidates

Karl Palmskog (Dec 19 2022 at 17:40):

in particular, we shouldn't have to refresh the 8.17 docker for the rc until 8.17.0 comes out (or there is an rc2, which hasn't happened yet)

Karl Palmskog (Dec 19 2022 at 17:46):

for example, see here for what generally happens to a Docker that uses a package that changes (it rebuilds the package and every dep in every CI run)

Théo Zimmermann (Dec 20 2022 at 10:20):

Théo Zimmermann (Dec 20 2022 at 10:21):

The principle with the rc1 is that after it is tagged, there is a commitment not to merge PRs with overlays. (The tag that was made for rc1 should still work for the final release.)

Théo Zimmermann (Dec 20 2022 at 10:21):

But if people start tagging before the rc1, then there is no way for the RM to signal that things are stable now.

Théo Zimmermann (Dec 20 2022 at 10:32):

I didn't include it in my list because since it has no changelog and no overlays, it seemed like it could easily be included between the rc1 and the final release.

Emilio Jesús Gallego Arias (Dec 20 2022 at 10:43):

My testing did go well and I'm convinced that the code is fine (both on wire protocol and UI) , however, we lack test-cases for many of the code paths, as Jim has noted, so it wouldn't hurt to have the CoqIDE fixes to see some testing just in case.

Théo Zimmermann (Dec 20 2022 at 11:13):

If what you are hoping for is user testing, then I'm afraid that the rc1 rarely gets any user testing (this was the starting point for moving from a beta to a rc BTW).

Pierre Roux (Dec 20 2022 at 11:16):

Emilio Jesús Gallego Arias (Dec 20 2022 at 11:52):

Indeed I'm not hoping for a lot of user testing, but I guess that should give us some more time in case a problem appears.

Karl Palmskog (Dec 20 2022 at 12:07):

Karl Palmskog (Dec 20 2022 at 12:08):

and I meant that bignums is special w.r.t. tagging, it should be obvious whether it has a chance of failing with v8.17 vs. 8.17+rc1, and it's present by default when testing rc1 via Docker

Pierre-Marie Pédrot (Dec 20 2022 at 12:12):

Karl Palmskog (Dec 20 2022 at 12:17):

if we want to make a serious effort with larger scale testing of the rc, that's fine by me, but please flag up how you want this to happen. Right now, I basically wait for the Docker with rc1 and then start to use this in every Coq project I (co-)maintain. But we could start pushing it more.

Karl Palmskog (Dec 20 2022 at 12:33):

@Emilio Jesús Gallego Arias so do you think there will be a SerAPI tag for the rc? If there won't be a tag, then we should discuss changes to the Docker setup with @Erik Martin-Dorel (e.g., possibly dropping the SerAPI-related packages from both rc and regular Coq Docker). I think it's very valuable to have SerAPI packages preinstalled due to Alectryon usage, but it's not an absolute requirement from my side.

Emilio Jesús Gallego Arias (Dec 20 2022 at 13:09):

Emilio Jesús Gallego Arias (Dec 20 2022 at 13:10):

in fact I think both you and Theo have push rights so feel free to push the tag when you need it

Emilio Jesús Gallego Arias (Dec 20 2022 at 13:10):

Karl Palmskog (Dec 20 2022 at 13:14):

Théo Zimmermann (Dec 20 2022 at 14:21):

Some of the PRs that I listed still have overlays for plugins in Coq's CI. This happens not to include bignums, but it could have.

Théo Zimmermann (Dec 20 2022 at 14:22):

Karl Palmskog (Dec 20 2022 at 15:01):

OK, I think you have to say something more specific than "user testing" if you mean interface-level testing.

Karl Palmskog (Dec 20 2022 at 15:01):

is there any manual test suite or similar for CoqIDE and/or VsCoq? Like, a list of typical workflows with specific clicks and keyboard commands, and expected results.

Théo Zimmermann (Dec 20 2022 at 15:07):

Anyway, my point was just not to expect such testing to happen, not that I wanted to act to make things change.

Karl Palmskog (Dec 20 2022 at 15:08):

OK, if there's nothing I think the minimum we do is just ask someone to run some basic commands in IDEs, in worst case we do it ourselves

Emilio Jesús Gallego Arias (Dec 20 2022 at 15:42):

Most of the testing we need IDE side could be automated in the test-suite, using fake_ide or a UI test system; for coq-lsp we are hoping to add a quite complete test-suite

Emilio Jesús Gallego Arias (Dec 20 2022 at 15:42):

Karl Palmskog (Dec 21 2022 at 12:23):

@Erik Martin-Dorel when we do the 8.17+rc1 Docker, would be very useful to have one with OCaml 5, e.g., coq-8.17-ocaml-5.0-flambda. Is this doable, and should I open an issue as reminder?

Théo Zimmermann (Dec 29 2022 at 17:21):

Karl Palmskog (Dec 29 2022 at 21:57):

is coq-stdlib really supposed to have this awkward non-Dune part in the build?

 [ "./configure"
    "-prefix" prefix
    "-mandir" man
    "-libdir" "%{lib}%/coq"
    "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed}
  ]
  [ make "dunestrap" "COQ_DUNE_EXTRA_OPT=-split" ]

Karl Palmskog (Dec 29 2022 at 22:02):

Guillaume Melquiond (Dec 30 2022 at 07:19):

We still need to create the module coq_config.ml (as well as a bunch of other files) before the compilation. In fact, even Dune creates that file by calling ./configure. But Dune does not call it with the arguments we want for the Opam package. So, we call it manually beforehand.

Karl Palmskog (Dec 30 2022 at 10:18):

are plugins supposed to start to depend directly on coq-core and coq-stdlib now in opam?

Guillaume Melquiond (Dec 30 2022 at 10:23):

Except for plugins that depend purely on coq-core, I would say no, as it would make writing package dependencies a bit painful, e.g., coq | (coq-core & coq-stdlib).

Karl Palmskog (Dec 30 2022 at 10:24):

hmm, but why would you need the coq | in an 8.17 plugin? The coq package is implicitly sufficient since it depends on coq-core/coq-stdlib.

Guillaume Melquiond (Dec 30 2022 at 10:25):

You are implicitly assuming that the plugin is not compatible with Coq 8.16 here.

Karl Palmskog (Dec 30 2022 at 10:26):

sure, but that's generally the case. Plugins I've worked with have been compatible across major versions maybe 1-2 times out of 20.

Guillaume Melquiond (Dec 30 2022 at 10:38):

But is that for a good reason? For example, the next Opam release of Bignums will be marked coq >= 8.17, but I would not be surprised if it was compatible with 8.16 too. So, are plugins really incompatible or is it just that people just assume that they are?

Karl Palmskog (Dec 30 2022 at 10:51):

my default assumption is that they are incompatible across major versions, yes. So by default, I set opam constraints for a single version. But there aren't really any adverse consequences to this, since we do one plugin release per major version anyway

Théo Zimmermann (Dec 30 2022 at 11:26):

It looks like the only three changes that were merged in bignums between 8.16 and 8.17 are indeed backward-compatible, but that's often not the case.

Pierre Roux (Dec 30 2022 at 11:44):

It also varies from plugin to plugin, paramcoq or coq-elpi for instance certainly wouldn't build on more than one version.

Karl Palmskog (Dec 30 2022 at 12:03):

@Emilio Jesús Gallego Arias fair warning that I plan to do some small fiddling with the SerAPI v8.17 branch so we can have tag to go in the 8.17+rc1 Docker image

Karl Palmskog (Dec 30 2022 at 12:09):

seems like the consensus is to continue to depend on coq in opam in nearly all places (e.g., I guess HoTT might want to go coq-core)

Ali Caglayan (Dec 30 2022 at 12:10):

HoTT cannot go coq-core because coq-core doesn't work out of the box despite the name.

Ali Caglayan (Dec 30 2022 at 12:10):

Karl Palmskog (Dec 30 2022 at 13:14):

I started looking at the changelog, and it's pretty weird to me that although -rectypes is no longer required as stated there, coq_makefile still seemingly uses it for ML code... intentional?

Gaëtan Gilbert (Dec 30 2022 at 13:18):

To avoid having to deal with backward compat issues
we could remove it from the default flags
feel free to make a PR (the coq_makefile flags come from configure.ml through a twisted process for historical reasons, so that's what you would edit)

Karl Palmskog (Dec 30 2022 at 13:20):

OK, will do. But bottom line, at least for plugins, it makes sense to drop it (-rectypes) everywhere?

Karl Palmskog (Dec 30 2022 at 13:20):

Gaëtan Gilbert (Dec 30 2022 at 13:56):

Karl Palmskog (Jan 02 2023 at 13:30):

can we maybe add some note and/or comment w.r.t. OCaml 5 performance for 8.17.0? I feel there is a risk of disappointed users creating lots of issues and forum questions. Fine with me if it's not done formally in release notes but in some forum like Discourse.

Karl Palmskog (Jan 02 2023 at 13:34):

Emilio Jesús Gallego Arias (Jan 02 2023 at 22:47):

@Karl Palmskog feel free to do whatever you need with the SerAPI repos, including a release , thanks!

For the 5.0 comment, I'm unsure what to say, IMHO it is still too early to claim anything. I think clearly OCaml 5.0 support should be marked "experimental" and the recommended setup for all users is 4.14 + flambda I think

Karl Palmskog (Jan 02 2023 at 22:50):

I tried Verdi Raft locally side by side 4.14+flambda and 5.0.0+flambda. The latter took several minutes longer in user time, consistent with the bench. I'm pretty certain people will see for themselves similar things after 8.17.0 is out.

Karl Palmskog (Jan 02 2023 at 22:51):

if it was only a few tens of seconds or even a minute or two, sure, but we are talking like 4-5 minutes slower.

Emilio Jesús Gallego Arias (Jan 02 2023 at 22:58):

Emilio Jesús Gallego Arias (Jan 02 2023 at 22:59):

I mean the statement is a bit too precise, we still don't understand why 5.0 is slower, could it be for the VM for example. So I think it good to be conservative and just set 5.0 as experimental

Karl Palmskog (Jan 02 2023 at 23:00):

I think most technical people when they hear "experimental" think "faster, but it may crash or behave strangely". This is not the case here, so that's why I think an explicit performance heads-up is warranted.

Emilio Jesús Gallego Arias (Jan 02 2023 at 23:00):

In my book when something is experimental == use at your own risk and don't expect it to work

Karl Palmskog (Jan 02 2023 at 23:00):

I've started using OCaml 5 for daily work, and functionally haven't had any trouble at all.

Karl Palmskog (Jan 02 2023 at 23:01):

Emilio Jesús Gallego Arias (Jan 02 2023 at 23:02):

The statement says "in particular as the OCaml 5 garbage collector improves" however we don't know if the GC is the culprit.

Emilio Jesús Gallego Arias (Jan 02 2023 at 23:02):

All we know is that it is experimental and shouldn't be used except for people willing to experiment

Emilio Jesús Gallego Arias (Jan 02 2023 at 23:03):

Karl Palmskog (Jan 02 2023 at 23:03):

Emilio Jesús Gallego Arias (Jan 02 2023 at 23:03):

Emilio Jesús Gallego Arias (Jan 02 2023 at 23:05):

Actually I was thinking to have an "enhaced" Coq opam package for 8.17, where I put a lot of the patches that are needed for coq-lsp , and why not, multithread proof checking

Emilio Jesús Gallego Arias (Jan 02 2023 at 23:06):

Emilio Jesús Gallego Arias (Jan 02 2023 at 23:09):

We will more the tracking of the 5.0 issues to github soon so everyone can comment

Maxime Dénès (Jan 03 2023 at 08:00):

It would be nice to avoid using the name coq-mt given the clash with CoqMT, IMHO.

Karl Palmskog (Jan 03 2023 at 09:46):

Karl Palmskog (Jan 03 2023 at 09:54):

Théo Zimmermann (Jan 03 2023 at 13:47):

@Emilio Jesús Gallego Arias Consider requesting a preview release to be included in the Coq Platform, like what Jim had done with the debugger before it was merged.

Karl Palmskog (Jan 03 2023 at 14:12):

@Erik Martin-Dorel all ingredients are there in the opam archive for a Docker for 8.17+rc1. Can/should I submit a docker-coq PR with the metadata for that?

Emilio Jesús Gallego Arias (Jan 03 2023 at 14:47):

LGTM @Karl Palmskog , tho I would maybe invert the way the content is delivered, the important thing for Coq users is in the last sentence, something like:

"Coq 8.17 supports OCaml 5.0, however such support is experimental and not recommended for end-users. In particular, we have observed some performance degradation and some Coq infrastructure such as the native reduciton tactics are not available when using OCaml 5.x"

Erik Martin-Dorel (Jan 03 2023 at 15:05):

Thanks @Karl Palmskog ! I'm precisely working on this (first, two builds of coqorg/base are on-going), I'll let you know in this thread!

Karl Palmskog (Jan 07 2023 at 12:26):

thanks to the 8.17 Docker, I've tested 8.17+rc1 in a large number of projects in Coq-community and elsewhere. Everything seems to work as expected.

Karl Palmskog (Jan 07 2023 at 12:29):

however, as yet there is no released version of MathComp compatible with 8.17, which restricts some of the scope of testing.

Erik Martin-Dorel (Jan 07 2023 at 17:20):

OK!
but I believe a MC release is pending… maybe @Cyril Cohen or @Pierre Roux could comment.

Karl Palmskog (Jan 09 2023 at 14:39):

looks like plugin releases for 8.17 are rolling in just fine, but we hope to see a certain parametric one...

Michael Soegtrop (Jan 16 2023 at 14:06):

Since I just released Coq Platform 2022.09.1 it is due time to look into Coq Platform 2023.03/04.

Since 8.17+rc1 is already tagged I guess I should send out the "please pick" issues asap?

Michael Soegtrop (Jan 16 2023 at 14:07):

Is there already a schedule for 8.17.0? I usually put the planned date into the "please pick" issues. Also the Coq Platform release name (2023.03 or 2023.04) depends on it.

Théo Zimmermann (Jan 16 2023 at 14:11):

The planned schedule was today IIRC, but it won't be met. So it is ASAP instead.

Michael Soegtrop (Jan 16 2023 at 14:28):

OK, I will start working on a beta pick for 8.17 then and do the issues as soon as I know the status.

Michael Soegtrop (Jan 16 2023 at 14:29):

Karl Palmskog (Jan 16 2023 at 14:30):

Michael Soegtrop (Jan 17 2023 at 09:34):

@Théo Zimmermann : looking at the release schedule of Coq 8.17, I guess we should target Coq Platform 2023.03 with a preview release in early February, a beta in early March and a release end of March or early April.

Théo Zimmermann (Jan 17 2023 at 10:14):

Théo Zimmermann (Jan 17 2023 at 10:16):

BTW, when you plan for something to be ready for end of March at the earliest, I would recommend naming it 2022.04, so that you have more chances of the name being adapted (and if you release before April, nobody is going to frown).

Michael Soegtrop (Jan 17 2023 at 10:19):

The preview has an incomplete and not maintainer approved package list (basically what works) which is mostly intended for maintainers to create the packages for the beta. The beta has a mostly complete and mostly maintainer approved package list.

Michael Soegtrop (Jan 17 2023 at 10:20):

For the preview I don't provide installers or a release. It is a state of Coq Platform main in which I drive the new package list as far as I can without support from the maintainers. The maintainers start from there.

Michael Soegtrop (Jan 17 2023 at 10:26):

So I guess the word "release" is misleading. It is essentially the point in time where I create the "please tag" issues.

Théo Zimmermann (Jan 17 2023 at 12:33):

OK thanks for clarifying. In this case, I think that we are already in a good enough state to start creating a preview. So this really depends on when you have time to allocate to this. As for the beta, it really depends on how many packages are not compatible yet in the preview and how long their maintainers need to create a tag.

Michael Soegtrop (Jan 17 2023 at 13:02):

Yes. It is about a day of work to create the initial pick. I try to squeeze it in either this week or early next week.

Théo Zimmermann (Jan 17 2023 at 13:25):

Would it help if we had some place, e.g., a wiki page, where we can collectively list known compatible tags or commits (in case there is no tag) of Coq Platform packages? I think a lot of such information is already available to opam archive and nixpkgs maintainers and it wouldn't be difficult to collect it.

Michael Soegtrop (Jan 17 2023 at 13:58):

I use "opam show" to inform myself about the status of a package. I think this is sufficient. The work starts when important packages are not compatible and need patching. The effort varies. For 8.16 the effort was large cause of the ocamlfind issues and the new rules for plugin naming rules. It can also be smooth.

Michael Soegtrop (Jan 30 2023 at 12:58):

@Théo Zimmermann : I just wanted to create a first pick for 8.17, but as it looks the 8.17.0 tag is not yet there. Should I base it on 8.17+rc1?

Théo Zimmermann (Jan 30 2023 at 12:59):

Michael Soegtrop (Jan 30 2023 at 13:03):

Théo Zimmermann (Jan 30 2023 at 13:04):

Théo Zimmermann (Jan 30 2023 at 13:05):

Paolo Giarrusso (Jan 30 2023 at 13:06):

Paolo Giarrusso (Jan 30 2023 at 13:08):

Ocaml code using "-Werror" (turning warnings into error) might fail on 4.14 deprecations, but they shouldn't use "Werror" anyway

Karl Palmskog (Feb 01 2023 at 20:15):

now it's finally possibly to test (dev package free) any project depending on MathComp with 8.17+rc1, since MC 1.16.0 is out on opam

Emilio Jesús Gallego Arias (Feb 09 2023 at 15:41):

Gaëtan Gilbert (Feb 09 2023 at 15:45):

IDK
it's not great to need overlays this late
maybe you can put the add_known_plugin and init_known_plugin APIs back for the backport

Gaëtan Gilbert (Feb 09 2023 at 15:46):

Emilio Jesús Gallego Arias (Feb 09 2023 at 15:46):

The overlays are not needed in the sense that both 8.17 branches already work, but in the CI are pinned

Emilio Jesús Gallego Arias (Feb 09 2023 at 15:46):

Gaëtan Gilbert (Feb 09 2023 at 15:46):

Emilio Jesús Gallego Arias (Feb 09 2023 at 15:47):

Yes, I agree, I could put the API back, but it is very trivial. IMO the overlays are a non-issue, the real question is whether the backport is risky, and the bug is important enough to risk it.

Emilio Jesús Gallego Arias (Feb 09 2023 at 15:47):

I am happy having users pin my branch, I was just wondering that maybe it would be best to directly backport this instead of doing all the "use my branch" stuff

Emilio Jesús Gallego Arias (Feb 09 2023 at 15:48):

Théo Zimmermann (Feb 09 2023 at 15:50):

Théo Zimmermann (Feb 09 2023 at 15:51):

I was not planning to backport this fix given that the bug has already been there for a long time and that we are very close to the final release.

Théo Zimmermann (Feb 09 2023 at 15:51):

I also would not like to break any plugin between the rc1 and the final release.

Emilio Jesús Gallego Arias (Feb 09 2023 at 15:55):

Hi @Théo Zimmermann , ok thanks for the info. (The plugin breakage is not a problem as can be trivially solved) but indeed I understand the reasons.

Gaëtan Gilbert (Feb 09 2023 at 16:24):

Gaëtan Gilbert (Feb 09 2023 at 16:26):

Théo Zimmermann (Feb 09 2023 at 16:54):

Théo Zimmermann (Feb 09 2023 at 16:55):

The conclusion from another Zulip discussion that I cannot locate ATM is revert the PRs that broke the things.

Théo Zimmermann (Feb 09 2023 at 17:25):

If someone wants to open a v8.17 PR reverting the two relevant PRs, that would be convenient.

Emilio Jesús Gallego Arias (Feb 09 2023 at 17:27):

Note that one of the reverts has to be partial, that is to say, only the coqide part, the fix in the lexer should stay

Théo Zimmermann (Feb 09 2023 at 19:11):

In that case, it would really be better if you could open the PR so that I don't mess it up.

Paolo Giarrusso (Feb 15 2023 at 02:10):

Ali Caglayan (Feb 15 2023 at 02:16):

Ali Caglayan (Feb 15 2023 at 02:17):

Hmm I guess there is a "set as latest release" option that needs to be ticked, but I don't have permission for that

Paolo Giarrusso (Feb 15 2023 at 02:24):

Ali Caglayan (Feb 15 2023 at 02:25):

Paolo Giarrusso (Feb 15 2023 at 02:25):

I went to the edit dialogue, changed nothing, and pressed "update release" (which probably I shouldn't have?)

Ali Caglayan (Feb 15 2023 at 02:26):

Paolo Giarrusso (Feb 15 2023 at 02:27):

Karl Palmskog (Feb 15 2023 at 07:46):

there is nothing strange to me with 8.1X+rc1 appearing before 8.1(X-1).1 or 8.1(X-1).2

Théo Zimmermann (Feb 15 2023 at 09:22):

The strange thing was rather that it wasn't appearing at all, if I understood Paolo correctly.

Paolo Giarrusso (Feb 15 2023 at 10:14):

Yep, because that made me think the RC hadn't been released yet, unlike I thought

Michael Soegtrop (Feb 28 2023 at 10:56):

The error is fine, but shouldn't we rework the message? It seems to fit more to the case when this was a warning.

Paolo Giarrusso (Feb 28 2023 at 11:16):

That's a good question, but IIRC the error can still be turned back into a warning, right?

Paolo Giarrusso (Feb 28 2023 at 11:17):

But it might be good to change "a future release" to a concrete one ("Coq 8.18"?), if that's been decided.

Théo Zimmermann (Feb 28 2023 at 11:42):

Michael Soegtrop (Feb 28 2023 at 14:03):

@Théo Zimmermann : I am about to create the "please tag" issues for all Coq Platform components. Usually I give a planned data for the .0 release in there. What date should I use?

Théo Zimmermann (Feb 28 2023 at 14:04):

The 8.17.0 release is expected very soon and has been delayed because of other things taking all of my bandwidth. I guess you could say ~2023-03-07 as a planned date (but expect it could come before or after depending on how long actually making the release happen takes).

Michael Soegtrop (Feb 28 2023 at 14:33):

Théo Zimmermann (Mar 06 2023 at 10:54):

Hello @Emilio Jesús Gallego Arias, don't forget about preparing this partial revert ASAP. Thanks!

Emilio Jesús Gallego Arias (Mar 06 2023 at 16:15):

Emilio Jesús Gallego Arias (Mar 06 2023 at 16:59):

If someone could prepare the revert so I can put just the fix after that'd be helpful

Emilio Jesús Gallego Arias (Mar 06 2023 at 17:04):

In particular prepare the revert and check that the behavior of that revert is OK

Emilio Jesús Gallego Arias (Mar 06 2023 at 17:04):

So then I have an easier job testing that the fix is not observable from CoqIDE / XML protocol clients

Rodolphe Lepigre (Mar 14 2023 at 12:36):

Paolo Giarrusso (Mar 14 2023 at 12:48):

Théo Zimmermann (Mar 14 2023 at 13:05):

Yes, basically there are regressions in CoqIDE that should be solved by https://github.com/coq/coq/pull/17348, but this breaks coq-lsp, so @Emilio Jesús Gallego Arias said he would refine this PR to avoid the regressions in CoqIDE without creating regressions in coq-lsp...

Théo Zimmermann (Mar 14 2023 at 13:05):

I've not merged https://github.com/coq/coq/pull/17343 yet to leave time for feedback on the exact message, but I can merge it at any time when the release is ready.

Théo Zimmermann (Mar 14 2023 at 13:07):

We might also want to fix https://github.com/coq/coq/issues/17374 by documenting the use of dune install better (@Rodolphe Lepigre you sound like a knowledgeable candidate to open a PR for this one).

Emilio Jesús Gallego Arias (Mar 14 2023 at 13:10):

Yes all we are missing is to ensure that #17348, which should revert 8.17 CoqIDE to 8.16 behavior is working fine.

Emilio Jesús Gallego Arias (Mar 14 2023 at 13:10):

Rodolphe Lepigre (Mar 14 2023 at 23:15):

Théo Zimmermann (Mar 15 2023 at 09:10):

Karl Palmskog (Mar 27 2023 at 16:07):

@Théo Zimmermann maybe I missed something, but did anyone "claim" the task of doing opam for 8.17.0 yet?

Karl Palmskog (Mar 27 2023 at 16:09):

(it's more work than usual due to the split packages, but I guess I'll do it if nobody else picks it up)

Théo Zimmermann (Mar 28 2023 at 07:12):

Karl Palmskog (Mar 28 2023 at 07:25):

OK, planning to do the opam-repository PRs, split for "pure Coq" and CoqIDE, tonight (and I will tag RM and Platform manager in PR)

Michael Soegtrop (Mar 28 2023 at 07:28):

Théo Zimmermann (Mar 28 2023 at 11:07):

Karl Palmskog (Mar 28 2023 at 12:57):

Karl Palmskog (Mar 28 2023 at 13:20):

can anyone more knowledgeable with Dune/OCaml/Coq-building help out in the opam-repository PR?

#=== ERROR while compiling coq-core.8.17.0 ====================================#
# context              2.2.0~alpha~dev | linux/ppc64 | ocaml-base-compiler.5.0.0 | pinned(https://github.com/coq/coq/archive/refs/tags/V8.17.0.tar.gz)
# path                 ~/.opam/5.0/.opam-switch/build/coq-core.8.17.0
# command              ~/.opam/opam-init/hooks/sandbox.sh build dune build -p coq-core -j 175 @install
# exit-code            1
# env-file             ~/.opam/log/coq-core-7-4e7521.env
# output-file          ~/.opam/log/coq-core-7-4e7521.out
### output ###
# File "topbin/dune", line 22, characters 7-15:
# 22 |  (name coqc_bin)
#             ^^^^^^^^
# Error: No rule found for topbin/coqc_bin.exe
# (cd _build/default/kernel/byterun && /usr/bin/gcc -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -D_FILE_OFFSET_BITS=64 -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -Wall -Wno-unused -g -O2 -g -I /home/opam/.opam/5.0/lib/ocaml -o coq_interp.o -c coq_interp.c)
# coq_interp.c: In function 'coq_interprete':
# coq_interp.c:817:11: warning: assignment discards 'volatile' qualifier from pointer target type [-Wdiscarded-qualifiers]
#   817 |         p = &Field(accu, 0);
#       |           ^

Karl Palmskog (Mar 28 2023 at 16:27):

the tests for the coqide-serveropam package seemingly doesn't work, as seen for example here:

[ERROR] The compilation of coqide-server.8.17.0 failed at "dune build -p coqide-server -j 11 @install @runtest".

#=== ERROR while compiling coqide-server.8.17.0 ===============================#
# context              2.1.4 | macos/x86_64 | ocaml-base-compiler.5.0.0 | pinned(https://github.com/coq/coq/archive/refs/tags/V8.17.0.tar.gz)
# path                 ~/.opam/5.0.0/.opam-switch/build/coqide-server.8.17.0
# command              ~/.opam/opam-init/hooks/sandbox.sh build dune build -p coqide-server -j 11 @install @runtest
# exit-code            1
# env-file             ~/.opam/log/coqide-server-86598-7e7888.env
# output-file          ~/.opam/log/coqide-server-86598-7e7888.out
### output ###
# File "test-suite/dune", line 11, characters 0-145:
# 11 | (rule
# 12 |  (targets bin.inc)
# 13 |  (action (with-stdout-to %{targets} (run ./ocaml_pwd.exe -quoted -trailing-slash ../../install/%{context_name}/bin/ ))))
# (cd _build/default/test-suite && ./ocaml_pwd.exe -quoted -trailing-slash ../../install/default/bin/) > _build/default/test-suite/bin.inc
# Fatal error: exception Sys_error("../../install/default/bin/: No such file or directory")
# File "test-suite/dune", line 7, characters 0-137:
# 7 | (rule
# 8 |  (targets libpath.inc)
# 9 |  (action (with-stdout-to %{targets} (run ./ocaml_pwd.exe -quoted ../../install/%{context_name}/lib/coq/ ))))
# (cd _build/default/test-suite && ./ocaml_pwd.exe -quoted ../../install/default/lib/coq/) > _build/default/test-suite/libpath.inc
# Fatal error: exception Sys_error("../../install/default/lib/coq/: No such file or directory")

Paolo Giarrusso (Mar 28 2023 at 17:03):

Based only on the quote, that test lacks dependencies, but building @install THEN @runtest (in a separate dune invocation) should fix that problem?

Paolo Giarrusso (Mar 28 2023 at 17:07):

But this is something I and @Rodolphe Lepigre need anyway soon, I might try later

Gaëtan Gilbert (Mar 28 2023 at 17:10):

I don't know how dune -p something @runtest works
which package does the test suite believe it belongs to?

Gaëtan Gilbert (Mar 28 2023 at 17:10):

is it going to try running the test suite for each package? but then coq-core should fail too?

Paolo Giarrusso (Mar 28 2023 at 17:15):

; Use summary.log as the target
(alias
 (name runtest)
 (package coqide-server)
 (deps test-suite/summary.log))

Paolo Giarrusso (Mar 28 2023 at 17:16):

AFAICT, -p foo means other packages are treated as non-existing — they must already be installed — but the above runtest is part of the coqide-server package. The target itself depends on all of coq:

(rule
 (targets summary.log)
 (deps
   ; [...]
  (package coq-core)
   (package coq-stdlib)
   ; For fake_ide
   (package coqide-server)

Paolo Giarrusso (Mar 28 2023 at 17:18):

$ dune clean
$ dune b test-suite/summary.log
      ocamlc test-suite/.ocaml_pwd.eobjs/byte/dune__exe__Ocaml_pwd.{cmi,cmo,cmt}
    ocamlopt test-suite/.ocaml_pwd.eobjs/native/dune__exe__Ocaml_pwd.{cmx,o}
    ocamlopt test-suite/ocaml_pwd.exe
File "test-suite/dune", line 11, characters 0-145:
11 | (rule
12 |  (targets bin.inc)
13 |  (action (with-stdout-to %{targets} (run ./ocaml_pwd.exe -quoted -trailing-slash ../../install/%{context_name}/bin/ ))))
   ocaml_pwd test-suite/bin.inc (exit 2)
Fatal error: exception Sys_error("../../install/default/bin/: No such file or directory")
File "test-suite/dune", line 7, characters 0-137:
7 | (rule
8 |  (targets libpath.inc)
9 |  (action (with-stdout-to %{targets} (run ./ocaml_pwd.exe -quoted ../../install/%{context_name}/lib/coq/ ))))
   ocaml_pwd test-suite/libpath.inc (exit 2)
Fatal error: exception Sys_error("../../install/default/lib/coq/: No such file or directory")
...

Paolo Giarrusso (Mar 28 2023 at 17:25):

OTOH, building @install first isn't enough — dune b -p coq-core,coq-stdlib,coqide-server @install; dune b -p coq-core,coq-stdlib,coqide-server @runtest also fails, if only on ../../install/default/lib/coq/. Ditto dune b --release @runtest.

Gaëtan Gilbert (Mar 28 2023 at 17:28):

Paolo Giarrusso (Mar 28 2023 at 17:28):

Paolo Giarrusso (Mar 28 2023 at 17:29):

that is, after dune b @install (which failed because gtk), runtest asked me to run make world

Paolo Giarrusso (Mar 28 2023 at 17:33):

but doesn't look like ../../install/default/lib/coq/ can work with -p coqide-server — the coq-stdlib is installed, not built locally

Paolo Giarrusso (Mar 28 2023 at 21:32):

it also seems that runtest should be a no-op on other packages (coq-core / coq-stdlib) — even after dune clean; make dunestrap; $ dune b -p coq-core,coq-stdlib @install, DUNE_CACHE=disabled dune b -p coq-core,coq-stdlib @runtest appears to do nothing

Karl Palmskog (Mar 29 2023 at 09:49):

@Théo Zimmermann here is a dilemma regarding packages that use Coq as a depopt in opam: even though the coq package may not be installed, they detect the coqc executable from coq-core and try to use Coq and may fail to build.

Théo Zimmermann (Mar 29 2023 at 09:50):

Well, add a version constraint for Coq 8.17.0 and let them deal with better detection mechanisms...

Théo Zimmermann (Mar 29 2023 at 09:50):

Karl Palmskog (Mar 29 2023 at 09:55):

just adding "coq" {< "8.17"} unfortunately doesn't work, it has to be a conflict with coq-core, that's the only thing I can think of

Théo Zimmermann (Mar 29 2023 at 10:17):

Gaëtan Gilbert (Mar 29 2023 at 10:22):

Is it possible to do a conditional conflict like "if coq-stdlib is not installed the conflict coq-core"?

Gaëtan Gilbert (Mar 29 2023 at 10:24):

Karl Palmskog (Mar 29 2023 at 11:25):

the whole update-revdep-packages thing is seemingly a bottomless rabbit hole. Now the packages I added conflicts with are failing due to not being compatible with OCaml 5, not being linted, etc.

Karl Palmskog (Mar 29 2023 at 14:08):

we got some help from the opam maintainers, so now there's a better chance of getting merged later today or tomorrow

Karl Palmskog (Mar 31 2023 at 05:44):

Karl Palmskog (Mar 31 2023 at 07:11):

@Emilio Jesús Gallego Arias we need a "proper" release of SerAPI for 8.17 in the OCaml opam repo for Docker images to work as expected, can I just make a release from the v8.17 SerAPI branch?

Karl Palmskog (Mar 31 2023 at 08:03):

@Michael Soegtrop all plugin packages and the like for 8.17 except for SerAPI should now be out on the released opam repo.

Michael Soegtrop (Mar 31 2023 at 10:19):

Thanks! I am currently doing a Coq Platform update sweep and plan to update to 8.17.0 and release a beta. There is one "full" package behind, though QuickChick. Otherwise the "opens" are mostly working packages without feedback.

Michael Soegtrop (Mar 31 2023 at 13:03):

I just finished the sweep. Missing are QuickChick (they are working on it, but no ETA), MetaCoq (ETA next week) and fiat-crypto (they are working on it, but no ETA). Otherwise I need to check if the update to 8.17.0 works, there are a few updates (VST, Eprover) and for a few working packages I didn't get feedback on the please pick issues (which is fine for a beta).

My plan is to do the beta without QuickChick, MetaCoq and FiatCrypto on Monday, but to push that they are there in 2 weeks.

Michael Soegtrop (Mar 31 2023 at 13:03):

There are btw. still CI issues (Windows and Snap), which I hope to fix over the weekend.

Stream: Coq devs & plugin devs

Topic: Coq Release 8.17

Emilio Jesús Gallego Arias (Nov 16 2022 at 19:08):

Théo Zimmermann (Nov 16 2022 at 19:17):

Emilio Jesús Gallego Arias (Nov 16 2022 at 19:36):

Emilio Jesús Gallego Arias (Nov 16 2022 at 19:36):

Olivier Laurent (Nov 16 2022 at 22:22):

Théo Zimmermann (Nov 17 2022 at 07:11):

Olivier Laurent (Nov 17 2022 at 07:29):

Emilio Jesús Gallego Arias (Nov 17 2022 at 20:11):

Théo Zimmermann (Nov 18 2022 at 09:46):

Olivier Laurent (Nov 18 2022 at 10:12):

Théo Zimmermann (Nov 21 2022 at 16:45):

Théo Zimmermann (Nov 21 2022 at 16:50):

Karl Palmskog (Nov 21 2022 at 16:53):

Théo Zimmermann (Nov 21 2022 at 17:00):

Théo Zimmermann (Nov 21 2022 at 17:00):

Théo Zimmermann (Nov 21 2022 at 17:01):

Karl Palmskog (Nov 21 2022 at 17:27):

Théo Zimmermann (Nov 21 2022 at 17:35):

Karl Palmskog (Nov 21 2022 at 17:48):

Théo Zimmermann (Nov 21 2022 at 17:49):

Karl Palmskog (Nov 21 2022 at 17:50):

Erik Martin-Dorel (Nov 21 2022 at 21:24):

Théo Zimmermann (Nov 22 2022 at 10:31):

Théo Zimmermann (Nov 27 2022 at 17:03):

Erik Martin-Dorel (Nov 28 2022 at 02:25):

Karl Palmskog (Dec 01 2022 at 13:49):

Karl Palmskog (Dec 01 2022 at 13:50):

Théo Zimmermann (Dec 01 2022 at 15:45):

Guillaume Melquiond (Dec 01 2022 at 16:15):

Gaëtan Gilbert (Dec 01 2022 at 16:18):

Guillaume Melquiond (Dec 01 2022 at 16:19):

Matthieu Sozeau (Dec 02 2022 at 10:19):

Emilio Jesús Gallego Arias (Dec 06 2022 at 13:30):

Théo Zimmermann (Dec 19 2022 at 15:30):

Emilio Jesús Gallego Arias (Dec 19 2022 at 16:02):

Karl Palmskog (Dec 19 2022 at 16:03):

Karl Palmskog (Dec 19 2022 at 16:08):

Emilio Jesús Gallego Arias (Dec 19 2022 at 16:32):

Emilio Jesús Gallego Arias (Dec 19 2022 at 16:32):

Pierre Roux (Dec 19 2022 at 17:05):

Karl Palmskog (Dec 19 2022 at 17:39):

Karl Palmskog (Dec 19 2022 at 17:40):

Karl Palmskog (Dec 19 2022 at 17:46):

Théo Zimmermann (Dec 20 2022 at 10:20):

Théo Zimmermann (Dec 20 2022 at 10:21):

Théo Zimmermann (Dec 20 2022 at 10:21):

Théo Zimmermann (Dec 20 2022 at 10:32):

Emilio Jesús Gallego Arias (Dec 20 2022 at 10:43):

Théo Zimmermann (Dec 20 2022 at 11:13):

Pierre Roux (Dec 20 2022 at 11:16):

Emilio Jesús Gallego Arias (Dec 20 2022 at 11:52):

Karl Palmskog (Dec 20 2022 at 12:07):

Karl Palmskog (Dec 20 2022 at 12:08):

Pierre-Marie Pédrot (Dec 20 2022 at 12:12):

Karl Palmskog (Dec 20 2022 at 12:17):

Karl Palmskog (Dec 20 2022 at 12:33):

Emilio Jesús Gallego Arias (Dec 20 2022 at 13:09):

Emilio Jesús Gallego Arias (Dec 20 2022 at 13:10):

Emilio Jesús Gallego Arias (Dec 20 2022 at 13:10):

Karl Palmskog (Dec 20 2022 at 13:14):

Théo Zimmermann (Dec 20 2022 at 14:21):

Théo Zimmermann (Dec 20 2022 at 14:22):

Karl Palmskog (Dec 20 2022 at 15:01):

Karl Palmskog (Dec 20 2022 at 15:01):

Théo Zimmermann (Dec 20 2022 at 15:07):

Théo Zimmermann (Dec 20 2022 at 15:07):

Karl Palmskog (Dec 20 2022 at 15:08):

Emilio Jesús Gallego Arias (Dec 20 2022 at 15:42):

Emilio Jesús Gallego Arias (Dec 20 2022 at 15:42):

Karl Palmskog (Dec 21 2022 at 12:23):

Théo Zimmermann (Dec 29 2022 at 17:21):

Karl Palmskog (Dec 29 2022 at 21:57):

Karl Palmskog (Dec 29 2022 at 22:02):

Guillaume Melquiond (Dec 30 2022 at 07:19):

Karl Palmskog (Dec 30 2022 at 10:18):

Guillaume Melquiond (Dec 30 2022 at 10:23):

Karl Palmskog (Dec 30 2022 at 10:24):

Guillaume Melquiond (Dec 30 2022 at 10:25):