Hi all,
Is there an easy way to debug issues when a library fails to load when the worker is starting up?
For context, this seems to be an issue with my OS (macOS Catalina fails; it works on my Arch Linux). At this time I'm just relying on Docker (which is fine), but at some point I'd like to use a non-dockerized version.
I tried to dump more info in the console by adding extra messages on coq-manager.js, but it seems useless.
Any thoughts?
Thanks!
Screen-Shot-2022-01-31-at-11.54.32-AM.png
Hi @Evariste G , umm, that's a bit strange of an error, what's the message log?
[between the UI and the worker I mean]
Debugging jsCoq [and Coq] init is a bit of a black art I'm afraid
Regarding the differences in OS setup, maybe there are some differences on the opam switch setup?
It would be great if we could implement an opam lock file [pull request for that super welcome]
Emilio Jesús Gallego Arias said:
Hi Evariste G , umm, that's a bit strange of an error, what's the message log?
Thanks for your quick reply! It seems to be some sort of "art", yep :sweat_smile:
There is no message at all - just what you see in the screenshot: Anomaly "Uncaught exception SyntaxError: Unexpected token ';'."
I know it was something during /lib/Coq/syntax/number_string_notation_plugin.cma loading....
But I was not able to track it.
@Evariste G if you reload the page, with the console open, you should see a log of messages that are sent to the workers, you see none?
Emilio Jesús Gallego Arias said:
Evariste G if you reload the page, with the console open, you should see a log of messages that are sent to the workers, you see none?
Do you mean the default Coq message
s and the Coq Feedback messages
?
If yes, unfortunately there is nothing
That's weird, I guess only option is to do a quick video call
I am at a loss on how to debug it otherwise
Thanks! Dont worry about it; maybe I can show you during the Hackathon. My Docker setup works like a charm :) I just asked in case anyone had seen it before. Thanks for the quick replies!
Sorry for having missed this exchange; have you figured out the ;
problem?
Shachar Itzhaky said:
Sorry for having missed this exchange; have you figured out the
;
problem?
No, I haven't (but I also haven't tried much since my Docker build works; so it seems to be some weird issue with my MacOS)
Weirdly not even 8.13 builds (it gives the same error)
Something odd happening when loading number_string_notation_plugin.cma
. I tried to track it backwards on coq-manager.js
, but I was not able to figure out how to get the failing event, which seems to happen after feedFileDependency
jsCoq handles dynamic loading of cma
by eval-ing the js_of_ocaml-compiled version of the code. The error seems to indicate that the resulting JS is somehow malformed. Which is weird. Can you try to look for init.coq-pkg
in your build directory? It is a zip archive and it should contain this file: Coq/syntax/number_string_notation_plugin.cma.js
.
Would be interesting to compare this file between your Docker build and the macOS build. The files should in principle be identical! The only quirk is that the macOS build uses a 64-bit target, which is mandated by Apple. But I am building on macOS and have not seen issues with it for some time.
Oh! I just got this error in my CI. Could be a js_of_ocaml regression? Funny thing is, it happens on my macOS and not on my Linux Docker :laughing: But at least I can investigate it now.
Interesting, we should start using the lockfiles so we pin the versions and we can track regressions a bit more easily
Yep; the Docker version automatically pulled js_of_ocaml 4.0.0 :scream: perhaps there are some breaking changes.
There is undeniably a semicolon that was not there before.
I follow JSOO development and they have been doing large changes
that's a prime suspect
Uh-oh! I was fooled by that one too - Both my docker image and my MacOS had jsoo 4.0.0, so I though that was not the source of the problem (because it worked fine on Docker....) Thanks @Shachar Itzhaky !
This .lock version works on my MacOS
depends: [
"base" {= "v0.14.3"}
"base-bigarray" {= "base"}
"base-bytes" {= "base"}
"base-threads" {= "base"}
"base-unix" {= "base"}
"biniou" {= "1.2.1"}
"cmdliner" {= "1.0.4"}
"conf-gmp" {= "4"}
"cppo" {= "1.6.8"}
"csexp" {= "1.5.1"}
"dune" {= "2.9.3"}
"dune-configurator" {= "2.9.3"}
"easy-format" {= "1.3.2"}
"js_of_ocaml" {= "3.11.0"}
"js_of_ocaml-compiler" {= "3.11.0"}
"js_of_ocaml-lwt" {= "3.11.0"}
"js_of_ocaml-ppx" {= "3.11.0"}
"lwt" {= "5.5.0"}
"lwt_ppx" {= "2.0.3"}
"menhir" {= "20211128"}
"menhirLib" {= "20211128"}
"menhirSdk" {= "20211128"}
"mmap" {= "1.1.0"}
"num" {= "1.4"}
"ocaml" {= "4.12.0"}
"ocaml-base-compiler" {= "4.12.0"}
"ocaml-compiler-libs" {= "v0.12.4"}
"ocaml-config" {= "2"}
"ocaml-options-vanilla" {= "1"}
"ocamlbuild" {= "0.14.0"}
"ocamlfind" {= "1.9.3"}
"ocplib-endian" {= "1.2"}
"parsexp" {= "v0.14.2"}
"ppx_derivers" {= "1.2.1"}
"ppx_deriving" {= "5.2.1"}
"ppx_deriving_yojson" {= "3.6.1"}
"ppx_import" {= "1.9.1"}
"ppx_sexp_conv" {= "v0.14.3"}
"ppxlib" {= "0.24.0"}
"result" {= "1.5"}
"seq" {= "base"}
"sexplib" {= "v0.14.0"}
"sexplib0" {= "v0.14.0"}
"stdlib-shims" {= "0.3.0"}
"uchar" {= "0.0.2"}
"yojson" {= "1.7.0"}
"zarith" {= "1.12"}
"zarith_stubs_js" {= "v0.14.1"}
]
Thanks for your help!
Cool. I have made a patch for it to work with 4.0.0 for 8.15. But I think we should fix the version to 3.11 in the 8.14 branch. @Emilio Jesús Gallego Arias would it be a good idea to commit the .lock
file?
For now, I have just added the constraint < "4"
to v8.14 and this patch to v8.15.
And thank you too @Evariste G for drawing our attention to the issue and for your interest in jsCoq :smile:
Sure @Shachar Itzhaky , we will do a couple of jsCoq hacking sessions next week, I'll try to improve a few bits of the toolchain setup hopefully.
Last updated: Sep 30 2023 at 16:01 UTC