-
Notifications
You must be signed in to change notification settings - Fork 188
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[BUG] Runtile failure with -linkall
since 5.1.0
#1641
Comments
Should be fixed by #1642. I took a quick look at goblint and have few remark/question
|
Thanks for the quick fix! (I didn't try it yet though.)
I don't recall the details, but I suspect it might have been an instance of ocaml/dune#4444. Nobody has checked whether our workaround is still needed since then, but that's for your pointer. I'll see if our workarounds can now be just removed or whether there's still some unreported issue.
Indeed, I was surprised to see it myself because we don't use it ourselves (instead we rely on
I don't know all the details, but it was added by a student in goblint/analyzer#315. There's some longer write-up about it as well: https://github.com/goblint/Zarith/raw/goblint/goblint/main.pdf. In our use case, we run Goblint natively and marshal out some data. Then Gobview, which is the js_of_ocaml front-end for it, can unmarshal this data in-browser and manipulate it with all existing Goblint code. I think the patching was necessary to make native marshaling output 32bit-sized values such that js_of_ocaml can unmarshal them correctly. |
I was able to use build info and dune site in #1643 |
Thanks for the explanation, I agree that there can be an issue trying to unmarshal a |
goblint-cil depends on dynlink https://github.com/goblint/cil/blob/develop/src/dune#L6 |
I tried goblint/analyzer@7b3b392 out in a fresh opam switch while making Gobview use the proper build-info and sites. I can reproduce the errors there. Upgrading dune from 3.6 to 3.7 seems to fix those actually, while still staying at This might've been the dune fix (also related to |
Describe the bug
Runtime failure during initialization when
-linkall
is used with the following exception:The large-ish project where this appears does not use dynlink in any way AFAIK. Only reference to dynlink is in
_build/default/.js/default/dynlink/dynlink.cma.js
, not any other libraries included into JS.Expected behavior
No failure.
Versions
The issue appears at js_of_ocaml 5.1.0. On 5.0.1 it as still fine:
-linkall
did not want to include that dynlink business.I suppose it's somehow related to #1378 but I don't really understand what it changed.
The text was updated successfully, but these errors were encountered: