Stream: Coq devs & plugin devs

Topic: 8.15.1 release


view this post on Zulip Théo Zimmermann (Mar 03 2022 at 17:13):

@Gaëtan Gilbert What's the current timeline for 8.15.1? https://github.com/coq/coq/wiki/Release-Schedule-for-Coq-8.15 says "if a sufficiently impactful bugfix appears before 8.16" but I think this is a clear yes now, and it would be too bad that the Coq Platform final release for 8.15 is still stuck on 8.15.0, wouldn't it? I expect that @Michael Soegtrop would like to release it soon.

view this post on Zulip Michael Soegtrop (Mar 03 2022 at 17:45):

For my own good I would actually like to have the CoqIDE fix in.

view this post on Zulip Michael Soegtrop (Mar 03 2022 at 17:46):

The 8.15.0 CoqIDE honestly doesn't leave a professional impression to users.

view this post on Zulip Guillaume Melquiond (Mar 03 2022 at 17:50):

That is the one I am using and I did not notice anything strange. Is it OS-dependent?

view this post on Zulip Michael Soegtrop (Mar 03 2022 at 17:53):

I am not sure - I am talking about (https://github.com/coq/coq/issues/15675) and (https://github.com/coq/coq/issues/15725).

view this post on Zulip Michael Soegtrop (Mar 03 2022 at 17:54):

The main issue is that when you click into accepted text and type at least the first character is lost.

view this post on Zulip Guillaume Melquiond (Mar 03 2022 at 17:58):

Indeed, I can reproduce it. Funnily enough, I have never experienced this issue, because my very first keypress is always "delete" or "backspace", and neither of them get lost.

view this post on Zulip Guillaume Melquiond (Mar 03 2022 at 18:00):

Actually, other keys are not lost either. So, it is really only the replacement of selected text that loses a keypress.

view this post on Zulip Guillaume Melquiond (Mar 03 2022 at 18:03):

By the way, I really don't see how the pull request https://github.com/coq/coq/pull/15714 could have fixed https://github.com/coq/coq/issues/15725 . Did someone actually confirm that it was fixed?

view this post on Zulip Guillaume Melquiond (Mar 03 2022 at 18:05):

(Otherwise, the point of releasing 8.15.1 is kind of moot.)

view this post on Zulip Karl Palmskog (Mar 03 2022 at 18:15):

@Guillaume Melquiond I think 8.15.1 is warranted even if the CoqIDE fix does not go in. Hugo fixed an important problem with Scheme: https://github.com/coq/coq/pull/15537

view this post on Zulip Paolo Giarrusso (Mar 03 2022 at 18:16):

make vok is also toast in 8.15.0

view this post on Zulip Paolo Giarrusso (Mar 03 2022 at 18:17):

(fix is already scheduled for 8.15.1)

view this post on Zulip Gaëtan Gilbert (Mar 03 2022 at 18:57):

after I come back from holiday, week after next

view this post on Zulip Michael Soegtrop (Mar 04 2022 at 06:54):

Guillaume Melquiond said:

By the way, I really don't see how the pull request https://github.com/coq/coq/pull/15714 could have fixed https://github.com/coq/coq/issues/15725 . Did someone actually confirm that it was fixed?

I did a local build of @Jim Fehrle 's branch (commit 917e93b8381dff6464c548536da50d3d7e21d246) and both issues appear to be fixed in it.

view this post on Zulip Jim Fehrle (Mar 04 2022 at 07:23):

@Guillaume Melquiond I'm happy to explain 15714 if you have questions.

view this post on Zulip Gaëtan Gilbert (Mar 18 2022 at 19:35):

I expect to tag 8.15.1 on monday
If a bugfix you want is not in the 8.15.1 milestone, NOW is the time to speak up

view this post on Zulip Michael Soegtrop (Mar 19 2022 at 09:39):

@Gaëtan Gilbert : perfect - I plan to do the Coq Platform 2022.03 release shortly after.

view this post on Zulip Michael Soegtrop (Mar 21 2022 at 21:13):

@Gaëtan Gilbert : I just wanted to ask what your plans are. Do you plan to postpone 8.15.1 cause of the unsoundness bug found by PMP? Or do you proceed as planned with 8.15.1 and do a 8.15.2 later? For Coq Platform this wouldn't be an issue, I can do a 2022.03.1 release any time.

view this post on Zulip Gaëtan Gilbert (Mar 21 2022 at 21:15):

postponed by 1 day

view this post on Zulip Gaëtan Gilbert (Mar 22 2022 at 13:03):

tagging when https://gitlab.com/coq/coq/-/pipelines/498169574 finishes

view this post on Zulip Michael Soegtrop (Mar 22 2022 at 13:26):

OK. The Coq platform release might take 2 days.

view this post on Zulip Gaëtan Gilbert (Mar 22 2022 at 16:19):

tagging when github works again

view this post on Zulip Gaëtan Gilbert (Mar 22 2022 at 16:38):

should be all done

view this post on Zulip Karl Palmskog (Mar 23 2022 at 10:07):

someone needs to bite the bullet and submit the opam packages. I will do it tonight March 23 unless someone else picks it up sooner...

view this post on Zulip Karl Palmskog (Mar 23 2022 at 10:08):

we should also cc @Erik Martin-Dorel so he knows that an update of the usual Docker images for 8.15.1 is imminent

view this post on Zulip Michael Soegtrop (Mar 24 2022 at 09:05):

@Gaëtan Gilbert , @Karl Palmskog : I still don't see a Coq 8.15.1 opam package or a PR for it. IMHO the release manager should do the opam package as well.

view this post on Zulip Karl Palmskog (Mar 24 2022 at 09:49):

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

I'll submit coqide.8.15.1 separately once coq.8.15.1 is merged.

view this post on Zulip Gaëtan Gilbert (Mar 24 2022 at 13:31):

it's merged

view this post on Zulip Michael Soegtrop (Mar 24 2022 at 13:39):

The Coq Platform release is almost finished. The main remaining working point is that I am still experimenting with Flocq3 / Flocq4. The other remaining items should be easy (like including ott, tests if certain things are indeed fixed upstream, ...). I expect that I have it tomorrow.

view this post on Zulip Karl Palmskog (Mar 24 2022 at 16:10):

what the heck is going on here for coqide.8.15.1 on OCaml 4.09:

#=== ERROR while compiling coqide.8.15.1 ======================================#
# context              2.1.2 | linux/x86_64 | ocaml-base-compiler.4.09.1 | pinned(https://github.com/coq/coq/archive/refs/tags/V8.15.1.tar.gz)
# path                 ~/.opam/4.09/.opam-switch/build/coqide.8.15.1
# command              ~/.opam/opam-init/hooks/sandbox.sh build dune build -p coqide -j 31
# exit-code            1
# env-file             ~/.opam/log/coqide-23418-66440a.env
# output-file          ~/.opam/log/coqide-23418-66440a.out
### output ###
#     ocamlopt ide/coqide/coqide_main.exe (exit 2)
# (cd _build/default && /home/opam/.opam/4.09/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -o ide/coqide/coqide_main.exe /home/opam/.opam/4.09/lib/coq-core/config/config.cmxa /home/opam/.opam/4.09/lib/coq-core/boot/boot.cmxa /home/opam/.opam/4.09/lib/ocaml/str.cmxa -I /home/opam/.opam/4.09/lib/ocaml /home/opam/.opam/4.09/lib/ocaml/unix.cmxa -I /home/opam/.opam/4.09/lib/ocaml /home/opam/.opam/4.09/lib/ocaml/threads/threads.cmxa -I /home/opam/.opam/4.09/lib/ocaml /home/opam/.opam/4.09/lib/coq-core/clib/clib.cmxa /home/opam/.opam/4.09/lib/coq-core/lib/lib.cmxa /home/opam/.opam/4.09/lib/coqide-server/protocol/protocol.cmxa /home/opam/.opam/4.09/lib/coqide-server/core/core.cmxa /home/opam/.opam/4.09/lib/ocaml/bigarray.cmxa -I /home/opam/.opam/4.09/lib/ocaml /home/opam/.opam/4.09/lib/cairo2/cairo.cmxa -I /home/opam/.opam/4.09/lib/cairo2 /home/opam/.opam/4.09/lib/lablgtk3/lablgtk3.cmxa -I /home/opam/.opam/4.09/lib/lablgtk3 /home/opam/.opam/4.09/lib/lablgtk3-sourceview3/lablgtk3_sourceview3.cmxa -I /home/opam/.opam/4.09/lib/lablgtk3-sourceview3 ide/coqide/coqide_gui.cmxa -I ide/coqide ide/coqide/.coqide_main.eobjs/native/dune__exe__Coqide_main.cmx)
# /usr/bin/ld: /home/opam/.opam/4.09/lib/lablgtk3/liblablgtk3_stubs.a(ml_gdk.o):/home/opam/.opam/4.09/.opam-switch/build/lablgtk3.3.1.1/_build/default/src/ml_gdk.c:51: multiple definition of `ml_table_extension_events'; /home/opam/.opam/4.09/lib/lablgtk3-sourceview3/liblablgtk3_sourceview3_stubs.a(ml_gtksourceview3.o):/home/opam/.opam/4.09/.opam-switch/build/lablgtk3-sourceview3.3.0.beta4/_build/default/src/ml_gdk.h:89: first defined here
# collect2: error: ld returned 1 exit status
# File "caml_startup", line 1:
# Error: Error during linking

see the full joblog here: https://opam.ci.ocaml.org/github/ocaml/opam-repository/commit/4f36fc0c55d72602e7c92dbedd49364f4bec1ce9/variant/opam-2.1,compilers,4.09,coqide.8.15.1,lower-bounds

view this post on Zulip Karl Palmskog (Mar 24 2022 at 16:13):

this was generated for the following PR: https://github.com/ocaml/opam-repository/pull/21007

view this post on Zulip Gaëtan Gilbert (Mar 24 2022 at 16:15):

failing only on ocaml 4.09
4.08 has lablgtl 3.1.1 instead of 3.1.2 but ocaml 4.10 has the same opam versions as 4.09

view this post on Zulip Karl Palmskog (Mar 24 2022 at 16:16):

I guess I could disable 4.09 in the package if we want this to go through, but far from ideal

view this post on Zulip Gaëtan Gilbert (Mar 24 2022 at 16:21):

why does it say lablgtk3.3.1.1 and lablgtk3-sourceview3.3.0.beta4 in the paths in the error?

view this post on Zulip Karl Palmskog (Mar 24 2022 at 16:23):

I think what is going is that they are testing a downgrade of lablgtk3

  - downgrade lablgtk3                3.1.2 to 3.1.1     [uses dune]
  - downgrade lablgtk3-sourceview3    3.1.2 to 3.0.beta4 [uses dune]

view this post on Zulip Gaëtan Gilbert (Mar 24 2022 at 16:24):

something about

ENV OPAMCRITERIA="+removed,+count[version-lag,solution]"
ENV OPAMEXTERNALSOLVER="builtin-0install"

view this post on Zulip Gaëtan Gilbert (Mar 24 2022 at 16:24):

is making it pick some strange versions

view this post on Zulip Karl Palmskog (Mar 24 2022 at 16:25):

should I add lower bound for "lablgtk3-sourceview3" then maybe? For example:

  "lablgtk3-sourceview3" {>= "3.1.2"}

view this post on Zulip Emilio Jesús Gallego Arias (Mar 24 2022 at 16:26):

That's lablgtk problem, not coqide's

view this post on Zulip Gaëtan Gilbert (Mar 24 2022 at 16:27):

https://github.com/ocaml/opam-repository/blob/master/packages/lablgtk3-sourceview3/lablgtk3-sourceview3.3.0.beta4/opam may have the wrong version constraint

view this post on Zulip Gaëtan Gilbert (Mar 24 2022 at 16:27):

see also https://github.com/ocaml/opam-repository/pull/20651

view this post on Zulip Gaëtan Gilbert (Mar 24 2022 at 16:28):

it should have ocaml < 4.09 or maybe lablggtk = version

view this post on Zulip Emilio Jesús Gallego Arias (Mar 24 2022 at 16:29):

Yes, thanks @Gaëtan Gilbert for the analysis, IMHO coqide can be merged and the gtk fix implemented in parallel

view this post on Zulip Emilio Jesús Gallego Arias (Mar 24 2022 at 16:29):

tho coqide / coq can have really independent releases as we discussed

view this post on Zulip Karl Palmskog (Mar 24 2022 at 16:29):

OK, would be great if someone with more OCaml reputation points and knowledge of lablgtk than me commented in the coqide PR for benefit of OCaml CI people

view this post on Zulip Emilio Jesús Gallego Arias (Mar 24 2022 at 16:30):

It would be great, but I don't think opam maintainers measure comments on OCaml reputation points or stuff like that. Anyone can just point out the problem @Gaëtan Gilbert analyzed.

view this post on Zulip Gaëtan Gilbert (Mar 24 2022 at 16:31):

I don't think I have rep points but I commented

view this post on Zulip Emilio Jesús Gallego Arias (Mar 24 2022 at 16:34):

Where are the rep points?

view this post on Zulip Karl Palmskog (Mar 24 2022 at 16:35):

I mean, if you maintain some high-profile package, CI maintainers are much more likely to give support

view this post on Zulip Karl Palmskog (Mar 24 2022 at 16:36):

so I mean points in a very figurative sense

view this post on Zulip Emilio Jesús Gallego Arias (Mar 24 2022 at 16:40):

I can see why you would think like that but I'm not sure this is how it works, or indeed for them, you are already a member of the Coq team so you are maintaining the Coq package

view this post on Zulip Michael Soegtrop (Mar 24 2022 at 17:44):

Karl Palmskog said:

should I add lower bound for "lablgtk3-sourceview3" then maybe? For example:

  "lablgtk3-sourceview3" {>= "3.1.2"}

I btw. have "coqide.8.15.1 lablgtk3.3.1.2" in Coq Platform. Is this appropriate? I don't require a specific lablgtk3-sourceview3 version.

view this post on Zulip Karl Palmskog (Mar 24 2022 at 17:48):

@Michael Soegtrop that seems to work according to the OCaml opam archive CI. Our problems were only with lablgtk3.3.0.X

view this post on Zulip Michael Soegtrop (Mar 24 2022 at 17:49):

Thanks! I don't quite remember why I pin lablgtk3, though.

view this post on Zulip Karl Palmskog (Mar 24 2022 at 18:51):

ping @Erik Martin-Dorel that the coq.8.15.1 package has been deployed and appears after opam update.

view this post on Zulip Karl Palmskog (Mar 24 2022 at 20:23):

unfortunately, the CI job still seems to fail with the same linking error. However, it's now a different lablgtk3 package involved:

  - downgrade lablgtk3                3.1.2 to 3.1.1     [uses dune]
  - downgrade lablgtk3-sourceview3    3.1.2 to 3.0.beta5 [uses dune]

Could it be that the same version error is in lablgtk3-sourceview3.3.0.beta5?

view this post on Zulip Michael Soegtrop (Mar 25 2022 at 10:00):

Just wanted to inform that the 8.15.1 release might take until Monday. QuickChick still doesn't work on Windows (it anyway only works in the Cygwin compile from sources mode because it needs ocamlc), but currently it doesn't even work there, because the PATH is stripped on the way and then it doesn't find some DLLs.

view this post on Zulip Karl Palmskog (Mar 25 2022 at 13:13):

the coqide.8.15.1 package has now been deployed (can be accessed after doing opam update)

view this post on Zulip Michael Soegtrop (Mar 26 2022 at 08:06):

Karl Palmskog said:

Michael Soegtrop that seems to work according to the OCaml opam archive CI. Our problems were only with lablgtk3.3.0.X

For the records: on macOS CoqIDE crashes with lablgtk3.3.1.1 in seconds, but works fine with lablgtk3.3.1.2. I just experienced this because I forgot to update labalgtk3 in my dev pick. I guess we should mention this in the opam file as lower bound for lablgtk3.

view this post on Zulip Karl Palmskog (Mar 26 2022 at 09:52):

in that case, I think the 3.1.2 lower bound should only be for macoS. According to CI, it works on Linuxes

view this post on Zulip Gaëtan Gilbert (Mar 26 2022 at 09:53):

CI doesn't run coqide, only compiles it

view this post on Zulip Karl Palmskog (Mar 26 2022 at 09:59):

OK, I can qualify to: it's likely to work on Linuxes

view this post on Zulip Karl Palmskog (Mar 26 2022 at 10:00):

hasn't macOS had these issues with CoqIDE for a long time on various lablgtk versions?

view this post on Zulip Michael Soegtrop (Mar 26 2022 at 10:57):

@Karl Palmskog : not that I am aware of.

view this post on Zulip Michael Soegtrop (Mar 29 2022 at 17:39):

@Karl Palmskog : one more note on lablgtk3: I have (since ever) a patch in there (see https://github.com/coq/platform/blob/main/opam/opam-repository/packages/lablgtk3/lablgtk3.3.1.1/files/0001-Add-function-channel_of_descr_socket-windows-has-dif.patch). I can't really tell why I didn't push this upstream - the patch is Windows specific and at least for 3.3.1.1 was required - need to check for 3.3.1.2.

view this post on Zulip Karl Palmskog (Mar 29 2022 at 17:48):

OK, if we want to do a change to the coqide.8.15.1 package with a lablgtk bound, then I think it should be parameterized with OS, I think this is written something like: {> "X.Y" & os = "macos"}

view this post on Zulip Karl Palmskog (Mar 29 2022 at 17:50):

hmm, maybe it should be: "package-name" {os != "macos" | (os = "macos" & > "X.Y")}

view this post on Zulip Michael Soegtrop (Mar 29 2022 at 19:18):

I am not sure we did sufficient testing with other lablgtk versions to really say something about it, so I would put the limits tighter. I would think most CoqIDE users are beginners and use CoqIDE from Coq Platform.

view this post on Zulip Karl Palmskog (Apr 01 2022 at 11:16):

@Erik Martin-Dorel any chance for an update of the 8.15 Docker image to 8.15.1? Can/should I submit a PR for that?

view this post on Zulip Erik Martin-Dorel (Apr 01 2022 at 11:39):

Karl Palmskog said:

Erik Martin-Dorel any chance for an update of the 8.15 Docker image to 8.15.1? Can/should I submit a PR for that?

Thanks Karl. The patch was easy, I've just pushed this commit:

https://github.com/coq-community/docker-coq/commit/873b71554901e0116aefd60af5d4ae94fa1724ad

triggering this docker-keeper pipeline:

https://gitlab.com/coq-community/docker-coq/-/pipelines/506834062

but I can't monitor this right now; I'll have another look tonight anyway.


Last updated: Feb 06 2023 at 19:03 UTC