Stream: Coq devs & plugin devs

Topic: Coq Release 8.17


view this post on Zulip Emilio Jesús Gallego Arias (Nov 16 2022 at 19:08):

Hi folks, when is the last day you will consider PRs for 8.17 milestone then?

view this post on Zulip Théo Zimmermann (Nov 16 2022 at 19:17):

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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 16 2022 at 19:36):

I will, thanks

view this post on Zulip Emilio Jesús Gallego Arias (Nov 16 2022 at 19:36):

Need to review them myself

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Olivier Laurent (Nov 17 2022 at 07:29):

But is this an issue if this removal only lands in Coq 8.18?

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).

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Nov 18 2022 at 09:46):

Olivier Laurent said:

But is this an issue if this removal only lands in Coq 8.18?

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).

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?

view this post on Zulip Olivier Laurent (Nov 18 2022 at 10:12):

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?

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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Nov 21 2022 at 17:00):

Yes, indeed. On the model of the coq.dev package.

view this post on Zulip Théo Zimmermann (Nov 21 2022 at 17:00):

The release notes are unusually terse about this step.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Nov 21 2022 at 17:27):

isn't that only for the dev image?

view this post on Zulip Théo Zimmermann (Nov 21 2022 at 17:35):

Well, isn't an image that corresponds to a branch always a dev image?

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Nov 21 2022 at 17:49):

:+1: please someone do it :star_struck:

view this post on Zulip Karl Palmskog (Nov 21 2022 at 17:50):

I'll do it tomorrow night unless someone beats me to it.

view this post on Zulip Erik Martin-Dorel (Nov 21 2022 at 21:24):

Théo Zimmermann said:

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?

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Théo Zimmermann (Dec 01 2022 at 15:45):

I think there is a chance, but that won't be an objective for 8.17.0.

view this post on Zulip 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.)

view this post on Zulip Gaëtan Gilbert (Dec 01 2022 at 16:18):

https://github.com/coq/coq/wiki/Coq-Call-2022-11-30 says

no-naked-pointers not an issue anymore

what changed?

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Dec 02 2022 at 10:19):

Corrected

view this post on Zulip Emilio Jesús Gallego Arias (Dec 06 2022 at 13:30):

Guillaume Melquiond said:

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.)

#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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip Karl Palmskog (Dec 19 2022 at 16:08):

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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 19 2022 at 16:32):

Can't we just pick the head of the v8.17 branch?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 19 2022 at 16:32):

For SerAPI I mean

view this post on Zulip Pierre Roux (Dec 19 2022 at 17:05):

I'm doing the bignums chores

view this post on Zulip Karl Palmskog (Dec 19 2022 at 17:39):

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

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip Théo Zimmermann (Dec 20 2022 at 10:20):

Karl Palmskog said:

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

Please don't.

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Dec 20 2022 at 10:32):

Emilio Jesús Gallego Arias said:

#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.

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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Pierre Roux (Dec 20 2022 at 11:16):

Karl Palmskog said:

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

here it is: https://github.com/coq/opam-coq-archive/pull/2421

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2022 at 11:52):

Théo Zimmermann said:

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).

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.

view this post on Zulip Karl Palmskog (Dec 20 2022 at 12:07):

we did actually test like 10+ projects in Coq-community with 8.16+rc1

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Dec 20 2022 at 12:12):

Worst case is that we release 8.17 with a known serious issue.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2022 at 13:09):

@Karl Palmskog there will be a tag for the RC if you folks need it, up to you

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2022 at 13:10):

format is quite easy I think

view this post on Zulip Karl Palmskog (Dec 20 2022 at 13:14):

OK, then I can push a SerAPI tag after Théo tags rc1

view this post on Zulip Théo Zimmermann (Dec 20 2022 at 14:21):

Karl Palmskog said:

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

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.

view this post on Zulip Théo Zimmermann (Dec 20 2022 at 14:22):

Karl Palmskog said:

we did actually test like 10+ projects in Coq-community with 8.16+rc1

We do test compatibility with CI, but here I was talking about testing CoqIDE.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Dec 20 2022 at 15:07):

No, there is none, unfortunately.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2022 at 15:42):

Otherwise development is not possible

view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (Dec 29 2022 at 17:21):

FYI the 8.17+rc1 tag has been set.

view this post on Zulip 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" ]

view this post on Zulip Karl Palmskog (Dec 29 2022 at 22:02):

(I was under the impression we were dropping the configures)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Guillaume Melquiond (Dec 30 2022 at 10:25):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Dec 30 2022 at 12:10):

There are still a few things to cleanup there that nobody has the time to do.

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Dec 30 2022 at 13:20):

(and compilation will fail if I really need it?)

view this post on Zulip Gaëtan Gilbert (Dec 30 2022 at 13:56):

yes

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Jan 02 2023 at 13:34):

for example:

The OCaml runtime system, and in particular its garbage collector, was completely rewritten for multicore support in OCaml 5.0.0. Hence, Coq performance when compiled with OCaml 5 may be slightly to significantly worse than when compiled with OCaml 4, depending on the Coq project. We expect Coq performance to improve with future releases of OCaml, in particular as the OCaml 5 garbage collector improves. If Coq performance is critical, we advise users to continue to compile Coq using OCaml 4 for the time being.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 02 2023 at 22:58):

Yes, 5.0 support is experimental it is normal

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Jan 02 2023 at 23:01):

to be frank, the experience is like a throttled 4.14.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jan 02 2023 at 23:03):

You can indeed say that performance will be wrose

view this post on Zulip Karl Palmskog (Jan 02 2023 at 23:03):

fine with me to drop the specifics about GC then

view this post on Zulip Emilio Jesús Gallego Arias (Jan 02 2023 at 23:03):

yup let's wait until the multicore team finished their analysis

view this post on Zulip Emilio Jesús Gallego Arias (Jan 02 2023 at 23:03):

just indeed say no one should use 5.0 for now except to experiment

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jan 02 2023 at 23:06):

so users could install coq-mt instead of coq if wanted

view this post on Zulip Emilio Jesús Gallego Arias (Jan 02 2023 at 23:06):

we will see tho

view this post on Zulip 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

view this post on Zulip Maxime Dénès (Jan 03 2023 at 08:00):

Emilio Jesús Gallego Arias said:

so users could install coq-mt instead of coq if wanted

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

view this post on Zulip Karl Palmskog (Jan 03 2023 at 09:46):

probably better to use something explicit like coq-multicore

view this post on Zulip Karl Palmskog (Jan 03 2023 at 09:54):

one more attempt:

The OCaml runtime system was completely rewritten for multicore support in OCaml 5.0.0. Hence, using OCaml 5 to compile Coq is considered experimental, and Coq performance may be worse than when compiled with OCaml 4. Consequently, if Coq stability and performance is critical, we advise users to continue to compile Coq using OCaml 4 for the time being.

view this post on Zulip Théo Zimmermann (Jan 03 2023 at 13:47):

Sounds good @Karl Palmskog!

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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"

view this post on Zulip Erik Martin-Dorel (Jan 03 2023 at 15:05):

Karl Palmskog said:

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?

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!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Erik Martin-Dorel (Jan 07 2023 at 17:20):

Karl Palmskog said:

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

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

view this post on Zulip 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...

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Jan 16 2023 at 14:11):

Is there already a schedule for 8.17.0?

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

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Jan 16 2023 at 14:29):

Btw: who is the release manager for 8.17? Emilio?

view this post on Zulip Karl Palmskog (Jan 16 2023 at 14:30):

Théo is the RM for 8.17. The backup (co-)RM is Gaëtan

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Jan 17 2023 at 10:14):

I'm confused, how are the preview and the beta different again?

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (Jan 30 2023 at 12:59):

Yes. Please base it on 8.17+rc1.

view this post on Zulip Michael Soegtrop (Jan 30 2023 at 13:03):

Should I update OCaml? I am currently on 4.13.1.

view this post on Zulip Théo Zimmermann (Jan 30 2023 at 13:04):

I think that people testing 4.14 have not reported any issue, so I'd say yes.

view this post on Zulip Théo Zimmermann (Jan 30 2023 at 13:05):

(This includes Coq's own CI BTW.)

view this post on Zulip Paolo Giarrusso (Jan 30 2023 at 13:06):

My reports should have linked issues that 4.14 fixes

view this post on Zulip Paolo Giarrusso (Jan 30 2023 at 13:06):

(I mean my issue/MRs on the platform)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 09 2023 at 15:41):

Hi folks, I was wondering whether https://github.com/coq/coq/pull/17200 would be considered for backport?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 09 2023 at 15:41):

cc: @Gaëtan Gilbert @Théo Zimmermann

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Feb 09 2023 at 15:46):

even then I don't know how interested @Théo Zimmermann is in new backports

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 09 2023 at 15:46):

I can update the refs

view this post on Zulip Gaëtan Gilbert (Feb 09 2023 at 15:46):

it's not great to need to update the refs this late

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 09 2023 at 15:48):

So far the new code has been working pretty well.

view this post on Zulip Théo Zimmermann (Feb 09 2023 at 15:50):

Sorry, I had missed the mention for some reason.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

I will just provide my own tree to users for now.

view this post on Zulip Gaëtan Gilbert (Feb 09 2023 at 16:24):

also what are we doing about https://github.com/coq/coq/issues/17023 (coqide tooltips)? is it blocker?

view this post on Zulip Gaëtan Gilbert (Feb 09 2023 at 16:26):

also should we open a 8.17.1 milestone?

view this post on Zulip Théo Zimmermann (Feb 09 2023 at 16:54):

Yes, we should.

view this post on Zulip Théo Zimmermann (Feb 09 2023 at 16:55):

Gaëtan Gilbert said:

also what are we doing about https://github.com/coq/coq/issues/17023 (coqide tooltips)? is it blocker?

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

view this post on Zulip Théo Zimmermann (Feb 09 2023 at 17:25):

Here: https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/Strange.20lexing.20error/near/326215929

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Feb 15 2023 at 02:10):

FWIW 8.17+rc1 lacks a pre-release on https://github.com/coq/coq/releases, like https://github.com/coq/coq/releases/tag/V8.16%2Brc1

view this post on Zulip Ali Caglayan (Feb 15 2023 at 02:16):

That's weird, it is there https://github.com/coq/coq/releases/tag/V8.17%2Brc1

view this post on Zulip Ali Caglayan (Feb 15 2023 at 02:16):

Not sure why it isn't shown in the main releases page

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Feb 15 2023 at 02:24):

uh, works for me now? https://github.com/coq/coq/releases

view this post on Zulip Ali Caglayan (Feb 15 2023 at 02:25):

Very weird, I guess somebody at Github was tweaking something

view this post on Zulip 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?)

view this post on Zulip Ali Caglayan (Feb 15 2023 at 02:26):

I guess that fixed it

view this post on Zulip Paolo Giarrusso (Feb 15 2023 at 02:27):

and "Latest" on https://github.com/coq/coq still says 8.16.1 _as it most likely should_ :-)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Feb 15 2023 at 10:14):

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

view this post on Zulip Michael Soegtrop (Feb 28 2023 at 10:56):

Working on the 2023.03 pick for 8.17, I see a lot of errors:

Error: The default value for hint locality is currently "local" in a section
and "global" otherwise, but is scheduled to change in a future release. For
the time being, adding hints outside of sections without specifying an
explicit locality attribute is therefore deprecated. It is recommended to use
"export" whenever possible. Use the attributes #[local], #[global] and
#[export] depending on your choice. For example: "#[export] Hint Unfold foo :
bar." [deprecated-hint-without-locality,deprecated]

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Feb 28 2023 at 11:42):

It is a warning. Just one that is made fatal by default.

view this post on Zulip Théo Zimmermann (Feb 28 2023 at 11:42):

And yes, future release should be the next one.

view this post on Zulip Théo Zimmermann (Feb 28 2023 at 11:42):

Please open an issue so this is tracked.

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip Michael Soegtrop (Feb 28 2023 at 14:33):

Thanks. I state this as "expected" date, so some deviation is OK.

view this post on Zulip Théo Zimmermann (Mar 06 2023 at 10:54):

Emilio Jesús Gallego Arias said:

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 06 2023 at 16:15):

I have not Théo, thanks for the reminder! Will likely happen tomorrow.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Rodolphe Lepigre (Mar 14 2023 at 12:36):

Just out of curiosity, any idea when the release is gonna happen?

view this post on Zulip Paolo Giarrusso (Mar 14 2023 at 12:48):

according to https://github.com/coq/coq/milestone/48, it seems Coq itself is basically done (up to https://github.com/coq/coq/pull/17343), and the blocker might be CoqIDE?

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 14 2023 at 13:10):

Well, "working fine" here means having the same bugs that 8.16

view this post on Zulip Rodolphe Lepigre (Mar 14 2023 at 23:15):

I just created https://github.com/coq/coq/pull/17383 for https://github.com/coq/coq/issues/17374.

view this post on Zulip Théo Zimmermann (Mar 15 2023 at 09:10):

Thanks a lot!

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Théo Zimmermann (Mar 28 2023 at 07:12):

Indeed! But no, nobody did.

view this post on Zulip 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)

view this post on Zulip Michael Soegtrop (Mar 28 2023 at 07:28):

A status update on Coq Platform:

So nothing serious, but it takes a bit of time.

view this post on Zulip Théo Zimmermann (Mar 28 2023 at 11:07):

sed 's/8.14/4.14/' in your message, I guess

view this post on Zulip Karl Palmskog (Mar 28 2023 at 12:57):

in case anyone not pinged is interested: https://github.com/ocaml/opam-repository/pull/23584

view this post on Zulip 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);
#       |           ^

view this post on Zulip 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")

should I disable the (Dune) tests in this package? Are they even meant to work?

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Mar 28 2023 at 17:07):

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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Mar 28 2023 at 17:15):

coq/dune:

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

view this post on Zulip 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)

view this post on Zulip Paolo Giarrusso (Mar 28 2023 at 17:18):

indeed, I just reproduced this without -p

$ 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")
...

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Mar 28 2023 at 17:28):

is that with dunestrap?

view this post on Zulip Paolo Giarrusso (Mar 28 2023 at 17:28):

just remembered, yeah

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Théo Zimmermann (Mar 29 2023 at 09:50):

(Maybe ping the maintainers to let them know of the problem.)

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Mar 29 2023 at 10:17):

Indeed, you're right!

view this post on Zulip 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"?

view this post on Zulip Gaëtan Gilbert (Mar 29 2023 at 10:24):

I guess not https://opam.ocaml.org/doc/Manual.html#opamfield-conflicts

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Mar 31 2023 at 05:44):

8.17.0 is finally out on opam (opam update)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kazuhiko Sakaguchi (Apr 27 2023 at 13:09):

Can we have a Zenodo entry for 8.17? https://zenodo.org/record/7313584

view this post on Zulip Théo Zimmermann (Apr 27 2023 at 13:43):

No, that's still on my to-do (but I had forgotten about it).


Last updated: May 31 2023 at 16:01 UTC