Théo Zimmermann (Mar 03 2022 at 17:13): 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.
Michael Soegtrop (Mar 03 2022 at 17:45):For my own good I would actually like to have the CoqIDE fix in.
Michael Soegtrop (Mar 03 2022 at 17:46):The 8.15.0 CoqIDE honestly doesn't leave a professional impression to users.
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?
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).
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.
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.
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.
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?
Guillaume Melquiond (Mar 03 2022 at 18:05):(Otherwise, the point of releasing 8.15.1 is kind of moot.)
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
Paolo Giarrusso (Mar 03 2022 at 18:16):make vok is also toast in 8.15.0
Paolo Giarrusso (Mar 03 2022 at 18:17):(fix is already scheduled for 8.15.1)
Gaëtan Gilbert (Mar 03 2022 at 18:57):after I come back from holiday, week after next
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.
Jim Fehrle (Mar 04 2022 at 07:23):@Guillaume Melquiond I'm happy to explain 15714 if you have questions.
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
Michael Soegtrop (Mar 19 2022 at 09:39):@Gaëtan Gilbert : perfect - I plan to do the Coq Platform 2022.03 release shortly after.
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.
Gaëtan Gilbert (Mar 21 2022 at 21:15):postponed by 1 day
Gaëtan Gilbert (Mar 22 2022 at 13:03):tagging when https://gitlab.com/coq/coq/-/pipelines/498169574 finishes
Michael Soegtrop (Mar 22 2022 at 13:26):OK. The Coq platform release might take 2 days.
Gaëtan Gilbert (Mar 22 2022 at 16:19):tagging when github works again
Gaëtan Gilbert (Mar 22 2022 at 16:38):should be all done
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...
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
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.
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.
Gaëtan Gilbert (Mar 24 2022 at 13:31):it's merged
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.
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
Karl Palmskog (Mar 24 2022 at 16:13):this was generated for the following PR: https://github.com/ocaml/opam-repository/pull/21007
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
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
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?
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]
something about
ENV OPAMCRITERIA="+removed,+count[version-lag,solution]"
ENV OPAMEXTERNALSOLVER="builtin-0install"
is making it pick some strange versions
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"}
That's lablgtk problem, not coqide's
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
Gaëtan Gilbert (Mar 24 2022 at 16:27):see also https://github.com/ocaml/opam-repository/pull/20651
Gaëtan Gilbert (Mar 24 2022 at 16:28):it should have ocaml < 4.09 or maybe lablggtk = version
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
Emilio Jesús Gallego Arias (Mar 24 2022 at 16:29):tho coqide / coq can have really independent releases as we discussed
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
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.
Gaëtan Gilbert (Mar 24 2022 at 16:31):I don't think I have rep points but I commented
Emilio Jesús Gallego Arias (Mar 24 2022 at 16:34):Where are the rep points?
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
Karl Palmskog (Mar 24 2022 at 16:36):so I mean points in a very figurative sense
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
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.
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
Michael Soegtrop (Mar 24 2022 at 17:49):Thanks! I don't quite remember why I pin lablgtk3, though.
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.
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?
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.
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)
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.
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
Gaëtan Gilbert (Mar 26 2022 at 09:53):CI doesn't run coqide, only compiles it
Karl Palmskog (Mar 26 2022 at 09:59):OK, I can qualify to: it's likely to work on Linuxes
Karl Palmskog (Mar 26 2022 at 10:00):hasn't macOS had these issues with CoqIDE for a long time on various lablgtk versions?
Michael Soegtrop (Mar 26 2022 at 10:57):@Karl Palmskog : not that I am aware of.
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.
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"}
Karl Palmskog (Mar 29 2022 at 17:50):hmm, maybe it should be: "package-name" {os != "macos" | (os = "macos" & > "X.Y")}
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.
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?
Erik Martin-Dorel (Apr 01 2022 at 11:39):Karl Palmskog said:
Erik Martin-Dorel any chance for an update of the
8.15Docker image to8.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: Oct 13 2024 at 01:02 UTC