Stream: Coq devs & plugin devs

Topic: 8.19.2


view this post on Zulip Gaëtan Gilbert (May 06 2024 at 11:08):

I plan to do a 8.19.2 release soon (this month)
If there are any fixes not in the milestone which you want there please say so here

view this post on Zulip Yann Leray (May 06 2024 at 11:20):

Any blocker against Fix RR hnf idempotency?
Nevermind, it's 8.19, this is not a problem there

view this post on Zulip Emilio Jesús Gallego Arias (May 06 2024 at 12:20):

@Gaëtan Gilbert what do you think about backporting the memprof-limits PR ?

That's all I can think of after reviewing the list of 8.20 PRs

view this post on Zulip Emilio Jesús Gallego Arias (May 06 2024 at 12:20):

https://github.com/coq/coq/pull/18906

view this post on Zulip Emilio Jesús Gallego Arias (May 06 2024 at 12:21):

https://github.com/coq/coq/pull/18893 is too small of a bugfix for us to bother IMO

view this post on Zulip Guillaume Melquiond (May 06 2024 at 13:03):

PRs potentially worth backporting: https://github.com/coq/coq/pull/18924 and https://github.com/coq/coq/pull/18883 and https://github.com/coq/coq/pull/18469

view this post on Zulip Hugo Herbelin (May 06 2024 at 18:39):

There were some regressions in coqide regaring error locating, esp. with utf8, but before backporting, one would need already a fix...

view this post on Zulip Emilio Jesús Gallego Arias (May 31 2024 at 15:42):

@Gaëtan Gilbert I backported the memprof-limits PR, I suggest we include it, as otherwise interruptions won't work for users, here is the backport https://github.com/ejgallego/coq/commit/d3208562933a0cc3d82b505061bb4a9f9900495d

If you agree, I'm happy to submit it to the main v8.19 branch

view this post on Zulip Gaëtan Gilbert (May 31 2024 at 15:58):

ok

view this post on Zulip Emilio Jesús Gallego Arias (Jun 03 2024 at 14:39):

Done, thanks @Gaëtan Gilbert

view this post on Zulip Gaëtan Gilbert (Jun 06 2024 at 11:22):

it would be nice if https://github.com/coq/coq/pull/19157 (changelog PR for master) got a quick assign & merge, then I can finish up the release
I don't think we will make a 8.19.3 so I won't make a milestone for it

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2024 at 11:35):

I have discovered a few bugs where Coq isn't still safe w.r.t. async interruptions, for example on Pcoq.unfreeze , but yeah, not sure they are worth a 8.19.3 update.

view this post on Zulip Gaëtan Gilbert (Jun 06 2024 at 11:35):

is it possible to be truly safe against async interruption?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2024 at 11:35):

It is still puzzling that we do restore Pcoq state twice on Vernacstate.Synterp.unfreeze (the state lives both there and in the summary).

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2024 at 11:37):

Yes it is @Gaëtan Gilbert , at least for the ones we use (memprof-limits) but we need to use the Masking.with_resource primitive of the lib, which I think would actually kind of make the codebase better.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2024 at 11:37):

I actually wanted to be do a large cleanup w.r.t. to this and some other stuff Coq is doing, but unfortunately my time ran out.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2024 at 11:39):

Already there are very good comments on memprof-limits code about how their approach doesn't work for other async interruptions, (but could be made to work), but I think in Coq the only interruptions that we need in that sense are the ones that memprof-limit supports, so we should be fine.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2024 at 11:39):

The new races are quite hard to try but of course I manage haha

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2024 at 11:39):

basically if we interrupt the freeze the grammar state is corrupted, and contrary to most other freezes, doing freeze again doesn't work

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2024 at 11:41):

So there are several fixes to this.

I guess Guillaume Munch-Maccagnoni could say more about your question @Gaëtan Gilbert but I think he has no Zulip account.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2024 at 14:34):

Anyways the only remaining bug I could spot is "when interrupted, Pcoq.freezewill leave the grammar state in an inconsistent status which cannot be repaired by calling Pcoq.freeze again"

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2024 at 14:34):

That's a bug IMO easy to fix in several ways

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2024 at 14:35):

Yesterday I did some kind of crazy testing interrupting Coq millions of times, in the server I loaded the full of HoTT, mathcomp-1, CompCert and Flocq so not too shabby IMHO

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2024 at 14:35):

Things look ready for multicore to me.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2024 at 14:44):

Actually the fact I managed to interrupt Pcoq.freeze tho seems to be telling us that it is again taking likely too much time.

It is true that we don't cache parsing so we call it very often in such a workload where multiple unrelated documents get schedules very often.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2024 at 14:45):

But maybe time to profile it again in such a load, the cost of Pcoq.freeze is basically linear right folks? (Or even worse)

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2024 at 15:33):

Emilio Jesús Gallego Arias said:

It is still puzzling that we do restore Pcoq state twice on Vernacstate.Synterp.unfreeze (the state lives both there and in the summary).

https://github.com/coq/coq/pull/19159 to investigate this.

view this post on Zulip Gaëtan Gilbert (Jun 07 2024 at 11:50):

should be ready to release once https://github.com/coq/coq/pull/19173 passes

view this post on Zulip Emilio Jesús Gallego Arias (Jun 07 2024 at 14:34):

@Gaëtan Gilbert see PR https://github.com/coq/coq/pull/19175

view this post on Zulip Emilio Jesús Gallego Arias (Jun 07 2024 at 14:35):

If it would be acceptable for you to ship that plus a couple of maskings for 8.19.2 let me know, I will submit a quick PR that fixes the race I detected upstream.

If that is not OK for 8.19.2, I will submit a deeper rework for master (and backport the fix to my 8.19+lsp branch for testing)

view this post on Zulip Emilio Jesús Gallego Arias (Jun 07 2024 at 14:36):

IMHO these bugs are good to fix ASAP, but indeed OMMV.

view this post on Zulip Gaëtan Gilbert (Jun 07 2024 at 14:38):

8.19.2 is frozen

view this post on Zulip Gaëtan Gilbert (Jun 10 2024 at 11:39):

It is tagged.
Does anyone want to do the opam packages?

view this post on Zulip Gaëtan Gilbert (Jun 14 2024 at 11:22):

https://github.com/ocaml/opam-repository/pull/26085

view this post on Zulip Karl Palmskog (Jun 20 2024 at 12:24):

ah, I think this is why I think one should normally never submit CoqIDE packages together with anything else in an opam repository PR. They will typically fail and block merging other packages. The remaining failures are seemingly just revdeps

view this post on Zulip Karl Palmskog (Jun 20 2024 at 12:27):

unfortunately I didn't have spare cycles to handle opam packaging this time, will try to do it for 8.20.0

view this post on Zulip Erik Martin-Dorel (Jun 20 2024 at 13:11):

Karl Palmskog said:

ah, I think this is why I think one should normally never submit CoqIDE packages together with anything else in an opam repository PR. They will typically fail and block merging other packages. The remaining failures are seemingly just revdeps

good point → you might want to add a note about that in https://github.com/coq/coq/blob/master/dev/doc/release-process.md, maybe? - my 2c

view this post on Zulip Gaëtan Gilbert (Jun 21 2024 at 14:38):

even without coqide it seems zarith doesn't work on windows
this seems to also be a problem for vscoq https://github.com/ocaml/opam-repository/pull/26087

view this post on Zulip Hugo Herbelin (Jun 21 2024 at 14:53):

It is maybe unrelated but I have failures installing zarith with opam on MacOS arm64 with emulated x86 (zarith seems to confuse different values of arch), to the point that I have to hack opam to bypass the default configuration.

view this post on Zulip Gaëtan Gilbert (Jun 24 2024 at 13:12):

main opam PR merged, coqide https://github.com/ocaml/opam-repository/pull/26139

view this post on Zulip Erik Martin-Dorel (Jun 24 2024 at 21:10):

coqorg/coq:8.19 and sibling images now ship Coq V8.19.2:
https://hub.docker.com/r/coqorg/coq#supported-tags
https://explore.ggcr.dev/?image=coqorg/coq:8.19

Regarding the update of the related stable mathcomp images, the build is ongoing:
https://gitlab.inria.fr/math-comp/docker-mathcomp/-/pipelines/996399

view this post on Zulip Karl Palmskog (Jun 26 2024 at 18:07):

@Erik Martin-Dorel putting this here since you are already talking about MathComp images. It looks like various MathComp dockers need a rebuild, they are re-installing a bunch of MathComp packages in CI runs: https://github.com/coq-community/graph-theory/actions/runs/9684414743/job/26722132412

view this post on Zulip Erik Martin-Dorel (Jun 26 2024 at 18:16):

Indeed, I see recompile conf-gmp 4 [upstream or system changes]; thanks @Karl Palmskog :+1: :+1:
(In this case, I think all images are concerned, so I'm going to rebuild them all.)

view this post on Zulip Karl Palmskog (Jun 26 2024 at 18:33):

@Erik Martin-Dorel for mathcomp-dev images, there is also this problem with coq-hierarchy-builder.dev

view this post on Zulip Erik Martin-Dorel (Jun 26 2024 at 18:34):

OK @Karl Palmskog, thanks;
And also there's this elpi problem with stable mathcomp + coq dev:
mathcomp/mathcomp:2.2.0-coq-dev FTBFS b/o elpi

view this post on Zulip Karl Palmskog (Jun 26 2024 at 19:47):

help appears to be on the way: https://github.com/coq/opam/pull/3056

view this post on Zulip Erik Martin-Dorel (Jun 26 2024 at 21:22):

FYI @Karl Palmskog: mathcomp pipeline & mathcomp-dev pipeline

view this post on Zulip Gaëtan Gilbert (Jun 29 2024 at 13:57):

coqide opam was merged


Last updated: Oct 13 2024 at 01:02 UTC