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....)

(Context: https://mit-plv.github.io/fiat-crypto/?argv=%5B%22unsaturated-solinas%22%2C%22--inline%22%2C%22--static%22%2C%22--use-value-barrier%22%2C%2225519%22%2C%2264%22%2C%22(auto)%22%2C%222%5E127-1%22%2C%22carry_mul%22%5D&interactive)

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