Stream: Coq devs & plugin devs

Topic: Where is the entry point to coqide?

view this post on Zulip Ali Caglayan (Feb 04 2022 at 14:47):

I would have thought that the first thing that gets called is in coqide_main.ml, but some other stuff seems to be called first. For example, if you unset DISPLAY and then OCAMLRUNPARAM=b dune exec -- coqide we have stuff being called from ideutils.ml first?!

view this post on Zulip Ali Caglayan (Feb 04 2022 at 14:47):

Fatal error: exception Gtk.Error("GtkMain.init: initialization failed\nml_gtk_init: initialization failed")
Raised at GtkMain.Main.init in file "src/gtkMain.ml", line 46, characters 8-69
Called from Ideutils in file "ide/coqide/ideutils.ml", line 13, characters 8-28

view this post on Zulip Ali Caglayan (Feb 04 2022 at 14:48):

How can I know what Ocaml is calling first?

view this post on Zulip Ali Caglayan (Feb 04 2022 at 14:48):

Removing the call from ideutils gives me a segmentation fault with no backtrace which is another story.

view this post on Zulip Guillaume Melquiond (Feb 04 2022 at 14:48):

Things are executed in linking order. So, ideutils.ml presumably appears before coqide_main.ml, and for good reasons.

view this post on Zulip Ali Caglayan (Feb 04 2022 at 14:52):

What good reason could there possibly be to be called before the entry point?

view this post on Zulip Guillaume Melquiond (Feb 04 2022 at 14:53):

You said it yourself: Because if you don't, you get a segfault.

view this post on Zulip Ali Caglayan (Feb 04 2022 at 14:54):

But that is only happening because other stuff is being called before the entry point

view this post on Zulip Ali Caglayan (Feb 04 2022 at 14:54):

I'm interested in making the entry point an actual entry point here

view this post on Zulip Ali Caglayan (Feb 04 2022 at 14:55):

Where can I read more about ocaml calling functions in linking order?

view this post on Zulip Guillaume Melquiond (Feb 04 2022 at 14:55):

Here is a simpler example. File A does let foo = ref 0 and file Main does let () = print_int !A.foo. If the main entrypoint was executed first, you would get a segfault, because A.foo would be a NULL pointer.

view this post on Zulip Gaëtan Gilbert (Feb 04 2022 at 14:57):

see also https://github.com/coq/coq/commit/bcbeac04993ffbad4f4432b646614491f2d8a5d5

view this post on Zulip Ali Caglayan (Feb 04 2022 at 15:02):

So how would we get the initialization centralized then? Is there a way to easily see what is getting called in linking order?

view this post on Zulip Ali Caglayan (Feb 04 2022 at 15:02):

@Guillaume Melquiond I don't disagree that your example makes sense, but I think it is bad practice, especially as an entry point to a program.

view this post on Zulip Guillaume Melquiond (Feb 04 2022 at 15:07):

Keep in mind that any declaration in an .mli file that is not of function type was necessarily initialized in linking order. There are presumably hundreds of instances in Coq. And it is not Coq being especially ugly. This is completely idiomatic in OCaml.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 16:15):

Does OCaml support relying on initialization order? I always thought that was explicitly undefined

view this post on Zulip Guillaume Melquiond (Feb 04 2022 at 16:20):

That is explicitly defined: "The order in which .cmx and .ml arguments are presented on the command line is relevant: compilation units are initialized in that order at run-time". And that is fortunate. Otherwise absolutely no toplevel definition would ever work.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 16:23):

So note that then we could have introduced some bug when porting to dune

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

as I'm not sure I preserved the link order

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

Yeah I got used to doing lib + small wrapper for executable so I don't care so much in the sense in my own programs I hope the init does commute

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

And usually I much prefer val init : unit -> unit for stuff that may be tricky

view this post on Zulip Ali Caglayan (Feb 04 2022 at 16:25):

So this means that because CoqIDE uses Gtk, it is impossible to call it without requiring everything in Gtk to run fine. This is unfortunate since it means we cannot coqide --help or coqide --version without an xserver...

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 16:25):

the thing is that when using a lib, if you don't do linkall you get into trouble if you abuse static init a lot

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 16:25):

for example

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

@Ali Caglayan I'm not expert but I'm not sure GTK does rely on static initialization a lot?

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

lablgtk examples require you to call init before they attempt to connect to the xserver IIRC

view this post on Zulip Guillaume Melquiond (Feb 04 2022 at 16:26):

Ali Caglayan said:

So this means that because CoqIDE uses Gtk, it is impossible to call it without requiring everything in Gtk to run fine. This is unfortunate since it means we cannot coqide --help or coqide --version without an xserver...

There is no fundamental reason we cannot. The parsing of command-line options (at least --help and --version) just need to happen earlier.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 16:27):

GMain.init ();

view this post on Zulip Ali Caglayan (Feb 04 2022 at 16:27):

@Guillaume Melquiond We literally cannot do it any earlier since Gtk initializing is called before the entry point

view this post on Zulip Guillaume Melquiond (Feb 04 2022 at 16:28):

Initialization happens in link order. Parsing of command-line options just need to be linked earlier.

view this post on Zulip Ali Caglayan (Feb 04 2022 at 16:28):

It is being called before commandline arguments are even parsed

view this post on Zulip Ali Caglayan (Feb 04 2022 at 16:30):

hmm ok so we make an ml file that gets linked first and parse arguments there

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

Umm, GMain.init _should_ not be called from static initializers

view this post on Zulip Ali Caglayan (Feb 04 2022 at 16:30):

How do I control the linking order?

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

I fail to see where it is called tho, but that's def a bad practice

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 16:31):

First you need to locate the bad part

view this post on Zulip Ali Caglayan (Feb 04 2022 at 16:31):

ideutils is being linked before coqide_main

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 16:31):

Aha!

view this post on Zulip Ali Caglayan (Feb 04 2022 at 16:31):

ln 13 in ideutils is the main Gtk init

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 16:31):

Sorry I see it now

view this post on Zulip Ali Caglayan (Feb 04 2022 at 16:31):

without it we get seg faults

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 16:31):

Instead of messing with the linking order

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 16:32):

call it from coqide_main

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 16:32):

that's a very bad practice

view this post on Zulip Ali Caglayan (Feb 04 2022 at 16:32):

We can't because it segfaults

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 16:32):

but could be painful to debug

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 16:33):

let me see

view this post on Zulip Ali Caglayan (Feb 04 2022 at 16:33):

No idea what to do with the info it spits out:

(process:151063): Gtk-CRITICAL **: 16:32:57.828: _gtk_style_provider_private_get_settings: assertion 'GTK_IS_STYLE_PROVIDER_PRIVATE (provider)' failed

(process:151063): Gtk-CRITICAL **: 16:32:57.828: _gtk_style_provider_private_get_settings: assertion 'GTK_IS_STYLE_PROVIDER_PRIVATE (provider)' failed

(process:151063): Gtk-CRITICAL **: 16:32:57.828: _gtk_style_provider_private_get_settings: assertion 'GTK_IS_STYLE_PROVIDER_PRIVATE (provider)' failed
Segmentation fault (core dumped)

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 16:33):

yeah some other static initializer is calling gtk code when it should not

view this post on Zulip Guillaume Melquiond (Feb 04 2022 at 16:33):

You cannot move it, since a few line later, the code does let cb = GData.clipboard Gdk.Atom.primary.

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

put that in a thunk or lazy value

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 16:35):

But indeed it will be painful to do the refactoring

view this post on Zulip Ali Caglayan (Feb 04 2022 at 16:36):

There are all sorts of things like that in ideutils

view this post on Zulip Ali Caglayan (Feb 04 2022 at 16:37):

We need to put those in an init step

view this post on Zulip Ali Caglayan (Feb 04 2022 at 16:37):

and call it from main

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 16:37):

yup that's the more correct way, if not, you can use the (modules ...) field to specify the linking order

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 16:38):

list the modules manually tho, I think, not sure the language is expressive enought

view this post on Zulip Ali Caglayan (Feb 04 2022 at 16:38):

Is ocaml backtrace able to show all the functions from the beginning of the run?

view this post on Zulip Ali Caglayan (Feb 04 2022 at 16:38):

That might help find which ones are being called

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 16:45):

@Ali Caglayan for that your best bet is ocamldebug or gdb

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 16:45):

I think [not a super expert on this as you have inferred]

view this post on Zulip Ali Caglayan (Feb 04 2022 at 16:53):

ocamldebug doesn't really give anything better

view this post on Zulip Ali Caglayan (Feb 04 2022 at 16:53):

Loading program... Fatal error: cannot load shared library dllcoqide_gui_stubs
Reason: dllcoqide_gui_stubs.so: cannot open shared object file: No such file or directory
Aborted (core dumped)

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 16:54):

That's a problem with the dll path

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 16:54):

it seems?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 16:54):

As far as I know ocamldebug allowed you to step the static init

view this post on Zulip Ali Caglayan (Feb 04 2022 at 16:56):

It doesn't give a backtrace or anything tho

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 16:58):

What about gdb?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 16:58):

Actually let me try myself

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 17:00):

I got this

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 17:00):

(gdb) bt
#0  0x00007ffff7823364 in  () at /lib/x86_64-linux-gnu/libgtk-3.so.0
#1  0x00007ffff76c9e0c in  () at /lib/x86_64-linux-gnu/libgtk-3.so.0
#2  0x00007ffff76ea307 in  () at /lib/x86_64-linux-gnu/libgtk-3.so.0
#3  0x00007ffff76d5492 in  () at /lib/x86_64-linux-gnu/libgtk-3.so.0
#4  0x00007ffff76ea232 in  () at /lib/x86_64-linux-gnu/libgtk-3.so.0
#5  0x00007ffff76ea28d in  () at /lib/x86_64-linux-gnu/libgtk-3.so.0
#6  0x00007ffff76d5ec6 in  () at /lib/x86_64-linux-gnu/libgtk-3.so.0
#7  0x00007ffff74f51a1 in g_type_create_instance () at /lib/x86_64-linux-gnu/libgobject-2.0.so.0
#8  0x00007ffff74d434d in  () at /lib/x86_64-linux-gnu/libgobject-2.0.so.0
#9  0x00007ffff74d5b45 in g_object_new_with_properties () at /lib/x86_64-linux-gnu/libgobject-2.0.so.0
#10 0x00007ffff74d66f1 in g_object_new () at /lib/x86_64-linux-gnu/libgobject-2.0.so.0
#11 0x00007ffff76f2c1f in  () at /lib/x86_64-linux-gnu/libgtk-3.so.0
#12 0x00007ffff78d1d8d in  () at /lib/x86_64-linux-gnu/libgtk-3.so.0
#13 0x00007ffff74f51a1 in g_type_create_instance () at /lib/x86_64-linux-gnu/libgobject-2.0.so.0
#14 0x00007ffff74d434d in  () at /lib/x86_64-linux-gnu/libgobject-2.0.so.0
#15 0x00007ffff74d5eb5 in g_object_newv () at /lib/x86_64-linux-gnu/libgobject-2.0.so.0
#16 0x0000555555a7e13d in ml_g_object_new (type=93825001579537, params=1) at ml_gobject.c:557
#17 0x000055555592c48d in camlGobject__unsafe_create_357 () at src/gobject.ml:208
#18 0x0000555555937849 in camlGtkObject__make_262 () at src/gtkObject.ml:30
#19 0x00005555559bdee5 in camlGMisc__fun_4006 () at src/gtkMiscProps.ml:268
#20 0x0000555555991546 in camlGContainer__fun_2289 () at src/gContainer.ml:84
#21 0x0000555555a39bb7 in camlCamlinternalLazy__force_lazy_block_166 () at camlinternalLazy.ml:31
#22 0x00005555558c8e20 in camlIdeutils__entry () at ide/coqide/ideutils.ml:33
#23 0x00005555558a9179 in caml_program ()
#24 0x0000555555ad372c in caml_start_program ()
#25 0x0000555555ab0fc4 in caml_startup_common (argv=0x7fffffffd6c8, pooling=<optimised out>, pooling@entry=0) at startup_nat.c:158
#26 0x0000555555ab100f in caml_startup_exn (argv=<optimised out>) at startup_nat.c:168
#27 caml_startup (argv=<optimised out>) at startup_nat.c:168
#28 0x00005555558a8482 in main (argc=<optimised out>, argv=<optimised out>) at main.c:41

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 17:00):

is IMHO usable

view this post on Zulip Ali Caglayan (Feb 04 2022 at 17:03):

So the program is entering at ideutils

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 17:04):

@Ali Caglayan got it running

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 17:04):

here's the diff

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 17:04):

https://pastebin.com/qc36mPnc

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 17:05):

that's a crude diff, a bit of refactoring would make it OK

view this post on Zulip Ali Caglayan (Feb 04 2022 at 17:06):

I'm not a big fan of making all of that lazy

view this post on Zulip Ali Caglayan (Feb 04 2022 at 17:06):

That means that all future calls need to also be lazy

view this post on Zulip Ali Caglayan (Feb 04 2022 at 17:07):

Which is easy to forget and unmaintainable imo

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 17:07):

Not sure what you mean, the right fix is of course to properly scope things

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 17:07):

but that's a lot of work

view this post on Zulip Ali Caglayan (Feb 04 2022 at 17:07):

That is the morally correct fix

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 17:08):

that's just a patch to blame the bad actors

view this post on Zulip Ali Caglayan (Feb 04 2022 at 17:08):

a more workable one might be to modify the linking order

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 17:08):

sure I'd be lovely to do the better patch, first is to identify them

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 17:08):

that's pretty fragile tho

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 17:08):

and a PITA for other reasons

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 17:08):

but I'm not opposed to it

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 17:08):

whatever works best for you

view this post on Zulip Guillaume Melquiond (Feb 04 2022 at 17:08):

-  let status_context = status#new_context ~name:"Messages" in
+  let status_context () = Lazy.(force status)#new_context ~name:"Messages" in

This cannot be correct. You are creating a new context at each call.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 17:09):

It's just a POC @Guillaume Melquiond to avoid the segfault

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 17:09):

indeed that's wrong

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 17:15):

Don't merge that diff indeed

Last updated: Sep 09 2024 at 04:02 UTC