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
Any blocker against Fix RR hnf idempotency?
Nevermind, it's 8.19, this is not a problem there
@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
https://github.com/coq/coq/pull/18906
https://github.com/coq/coq/pull/18893 is too small of a bugfix for us to bother IMO
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
There were some regressions in coqide regaring error locating, esp. with utf8, but before backporting, one would need already a fix...
@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
ok
Done, thanks @Gaëtan Gilbert
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
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.
is it possible to be truly safe against async interruption?
It is still puzzling that we do restore Pcoq
state twice on Vernacstate.Synterp.unfreeze
(the state lives both there and in the summary).
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.
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.
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.
The new races are quite hard to try but of course I manage haha
basically if we interrupt the freeze
the grammar state is corrupted, and contrary to most other freezes, doing freeze
again doesn't work
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.
Anyways the only remaining bug I could spot is "when interrupted, Pcoq.freeze
will leave the grammar state in an inconsistent status which cannot be repaired by calling Pcoq.freeze
again"
That's a bug IMO easy to fix in several ways
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
Things look ready for multicore to me.
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.
But maybe time to profile it again in such a load, the cost of Pcoq.freeze
is basically linear right folks? (Or even worse)
Emilio Jesús Gallego Arias said:
It is still puzzling that we do restore
Pcoq
state twice onVernacstate.Synterp.unfreeze
(the state lives both there and in the summary).
https://github.com/coq/coq/pull/19159 to investigate this.
should be ready to release once https://github.com/coq/coq/pull/19173 passes
@Gaëtan Gilbert see PR https://github.com/coq/coq/pull/19175
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)
IMHO these bugs are good to fix ASAP, but indeed OMMV.
8.19.2 is frozen
It is tagged.
Does anyone want to do the opam packages?
https://github.com/ocaml/opam-repository/pull/26085
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
unfortunately I didn't have spare cycles to handle opam packaging this time, will try to do it for 8.20.0
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
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
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.
main opam PR merged, coqide https://github.com/ocaml/opam-repository/pull/26139
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
@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
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.)
@Erik Martin-Dorel for mathcomp-dev images, there is also this problem with coq-hierarchy-builder.dev
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
help appears to be on the way: https://github.com/coq/opam/pull/3056
FYI @Karl Palmskog: mathcomp pipeline & mathcomp-dev pipeline
coqide opam was merged
Last updated: Oct 13 2024 at 01:02 UTC