Stream: Coq users

Topic: Extraction and js_of_ocaml

view this post on Zulip Jason Gross (Nov 18 2023 at 05:32):

Does anyone have suggestions for avoiding "too much recursion" errors from firefox when running extracted OCaml code compiled with js_of_ocaml? (Should I be asking this on the jsCoq channel?)

(Strangely, if I invoke the same OCaml function twice at the same time from javascript, this sometimes avoids the recursion error....)


view this post on Zulip Evan Marzion (Nov 18 2023 at 07:27):

I recently dealt with some confusing issues involving stack overflows and js_of_ocaml (if I moved the definition of the troublesome function from the extracted code into the hand-written ocaml the problem went away, the function itself was completely innocuous, etc.) and for some reason when I used Separate Extraction the problems went away. I guess something weird happens with how js_of_ocaml compiles modules. If there isn't any obvious non-tail-recursiveness that could be causing the issues, using Separate Extraction might be worth a shot.

Last updated: Jun 13 2024 at 19:02 UTC