Closed ejgallego closed 4 years ago
Is it correct that some apps that worked in beta6 and/or beta7 will break? What will be the breakage symptoms?
Also, it'd be great to know the impact on opam packages, especially for Coq 8.10.{0,1}. Should they just blacklist beta7?
Is it correct that some apps that worked in beta6 and/or beta7 will break? What will be the breakage symptoms?
Only those that are using -linkall
, which should not be a lot. Linkall is kinda dangerous anyways.
More precisely, lablgtk was never intended to be used with linkall. And very few packages use lablgtk3 anyway...
However, if you remove gtkInit.ml
and gtkThInit.ml
, this should probably be documented in README.md
.
There is a typo in the GtkThread
code (in the Windows port section, but this is not limited to Windows).
#threads
should be #thread
.
In the current version it seems that the thread is automatically started, but wouldn't you need to add a start ()
line if you remove gtkThInit.cmo
?
However, if you remove
gtkInit.ml
andgtkThInit.ml
, this should probably be documented inREADME.md
.
Already it doesn't mention them.
There is a typo in the
GtkThread
code (in the Windows port section, but this is not limited to Windows).#threads
should be#thread
.
Indeed.
In the current version it seems that the thread is automatically started, but wouldn't you need to add a
start ()
line if you removegtkThInit.cmo
?
Yes, the Linux version is correct, I forgot to check the example in my windows VM, sorry.
PR updated with errors fixed as suggested by @garrigue ; testing on my Win VM.
This appears to indeed fix coq/coq#11217. To sum up the impact for packagers, assuming beta8 is released with this fix:
I merged, and updated the instructions in README.md
after merging.
I checked that the instructions for MacOS work, but there is a bad side-effect: the new toplevel loop is not handled by utop. Do you know a way to do this in utop without losing the connection?
I didn't check on Windows.
Thanks @garrigue .
I checked that the instructions for MacOS work, but there is a bad side-effect: the new toplevel loop is not handled by utop. Do you know a way to do this in utop without losing the connection?
What do you exactly mean by losing the connection?
The toplevel is no longer handled by utop. So you lose editing, completion, etc...
Just try executing dune utop src
and input the commands I indicate for MacOS.
It should work on any machine (no need of MacOS to run it).
I see what you mean now, thanks. I'm not so familiar with the utop API but in principle it should be possible to call the utop toplevel back too I think.
We could maybe create a custom toplevel as explained here
This certainly works [on linux]:
let thread = Thread.create (fun () -> UTop_main.main) ()
and () = GtkThread.main ();;
Thanks. I've update README.md
accordingly.
Should I release beta8 now ?
Should I release beta8 now ?
Looks fine I think!
This fixes a bug introduced in #77 where clients using
-linkall
would doubly-link the initializers; moreover, we favor these days explicit initialization calls.See also https://github.com/coq/coq/issues/11217 , which this PR should fix.
I have updated the linking call in the examples that already perform the proper call to
GMain.init ()
Note that we could easily ship libraries
lablgtk3.init
and`lablgtk3.init-thread
for linking if we wanted, but IMO not worth it.