Evariste G (Jan 31 2022 at 17:00): Evariste G (Jan 31 2022 at 17:00):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
Emilio Jesús Gallego Arias (Jan 31 2022 at 17:02):Hi @Evariste G , umm, that's a bit strange of an error, what's the message log?
Emilio Jesús Gallego Arias (Jan 31 2022 at 17:03):[between the UI and the worker I mean]
Emilio Jesús Gallego Arias (Jan 31 2022 at 17:03):Debugging jsCoq [and Coq] init is a bit of a black art I'm afraid
Emilio Jesús Gallego Arias (Jan 31 2022 at 17:04):Regarding the differences in OS setup, maybe there are some differences on the opam switch setup?
Emilio Jesús Gallego Arias (Jan 31 2022 at 17:04):It would be great if we could implement an opam lock file [pull request for that super welcome]
Evariste G (Jan 31 2022 at 17:17):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.
Emilio Jesús Gallego Arias (Jan 31 2022 at 17:40):@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?
Evariste G (Jan 31 2022 at 18:36):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 messages and the Coq Feedback messages?
If yes, unfortunately there is nothing
Emilio Jesús Gallego Arias (Jan 31 2022 at 18:43):That's weird, I guess only option is to do a quick video call
Emilio Jesús Gallego Arias (Jan 31 2022 at 18:43):I am at a loss on how to debug it otherwise
Evariste G (Jan 31 2022 at 18:46):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!
Shachar Itzhaky (Feb 05 2022 at 19:54):Sorry for having missed this exchange; have you figured out the ; problem?
Evariste G (Feb 06 2022 at 20:07):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
Shachar Itzhaky (Feb 06 2022 at 20:13):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.
Shachar Itzhaky (Feb 08 2022 at 09:57):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.
Emilio Jesús Gallego Arias (Feb 08 2022 at 10:06):Interesting, we should start using the lockfiles so we pin the versions and we can track regressions a bit more easily
Shachar Itzhaky (Feb 08 2022 at 13:21):Yep; the Docker version automatically pulled js_of_ocaml 4.0.0 :scream: perhaps there are some breaking changes.
Shachar Itzhaky (Feb 08 2022 at 14:52):There is undeniably a semicolon that was not there before.
Emilio Jesús Gallego Arias (Feb 08 2022 at 16:17):I follow JSOO development and they have been doing large changes
Emilio Jesús Gallego Arias (Feb 08 2022 at 16:17):that's a prime suspect
Evariste G (Feb 08 2022 at 17:02):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!
Shachar Itzhaky (Feb 08 2022 at 17:33):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?
Shachar Itzhaky (Feb 08 2022 at 17:46):For now, I have just added the constraint < "4" to v8.14 and this patch to v8.15.
Shachar Itzhaky (Feb 08 2022 at 17:57):And thank you too @Evariste G for drawing our attention to the issue and for your interest in jsCoq :smile:
Emilio Jesús Gallego Arias (Feb 10 2022 at 20:23):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