Shachar Itzhaky (May 08 2021 at 13:28): Shachar Itzhaky (May 08 2021 at 13:28):I vaguely remember having discussing this — sometimes when you Require multiple modules, you get a stack overflow. e.g. in the landing page, this used to work (in 8.12):
From Coq Require Import ssreflect ssrfun ssrbool.
Now (8.13, https://coq-next.now.sh) we get a stack overflow. So I changed the landing page by splitting the Require into two Requires. It's a bit ugly. I think there was a patch with List.fold_left or something?
Emilio Jesús Gallego Arias (May 08 2021 at 13:32):There was a patch indeed, but there could be a few things.
Emilio Jesús Gallego Arias (May 08 2021 at 13:35):I don't get a stack overflow tho in chrome
Emilio Jesús Gallego Arias (May 08 2021 at 13:36):so it could be some Safari update?
Emilio Jesús Gallego Arias (May 08 2021 at 13:36):First thing to see if just Require without the import creates the problem
Emilio Jesús Gallego Arias (May 08 2021 at 13:37):if the problem is in require, the code path there is simple
Emilio Jesús Gallego Arias (May 08 2021 at 13:37):if it is in import, the codepath is also not too complex, basically an iteration too add names to the "Nametab"
Shachar Itzhaky (May 08 2021 at 14:19):Ok it did happen to me on Chrome but perhaps Chrome for Mac is a bit different. Safari is actually the best so far in my experience, as there is some tail-call optimization going on in their implementation.
Emilio Jesús Gallego Arias (May 08 2021 at 14:22):Let me try with a different chrome version
Emilio Jesús Gallego Arias (May 08 2021 at 14:23):Does removing the import help?
Emilio Jesús Gallego Arias (May 08 2021 at 14:23):All the 3 chrome versions I have [stable, beta, dev] do work fine :S
Emilio Jesús Gallego Arias (May 08 2021 at 14:24):If you do the trick of re-executing the problematic sentence a few times, does it work?
Shachar Itzhaky (May 08 2021 at 16:13):Ah yes. Both removing the import and re-executing the sentence a second time work.
Shachar Itzhaky (May 08 2021 at 16:35):Emilio Jesús Gallego Arias said:
All the 3 chrome versions I have [stable, beta, dev] do work fine :S
Oh also I am using the arm64 build :scream:
Emilio Jesús Gallego Arias (May 08 2021 at 18:26):If re-executing works it is just the JIT engine not triggering ; against that little we can do other than move to WASM I understand
Emilio Jesús Gallego Arias (May 08 2021 at 18:26):Let me check the Import code just out of curiosity.
Emilio Jesús Gallego Arias (May 08 2021 at 18:31):But indeed you have the patch in master to this code
Emilio Jesús Gallego Arias (May 08 2021 at 18:31):let import_modules ~export mpl =
let _,objs = List.fold_right collect_module_objects mpl (MPmap.empty, []) in
List.iter (fun (f,o) -> open_object f 1 o) objs;
if export then Lib.add_anonymous_entry (Lib.Leaf (ExportObject { mpl }))
so if we replace the fold_right by a fold_left + reverse should work but see the master patch for the side effect semantics
Emilio Jesús Gallego Arias (May 08 2021 at 18:33):Not sure actually how the version in master will behave with jsoo :S
Emilio Jesús Gallego Arias (May 08 2021 at 18:33):Wouldn't bet an ice cream that master is going to be an improvement for this code
Shachar Itzhaky (May 08 2021 at 21:28):Huh, interesting. So you're saying fold_right_cps is in fact useless since jsoo will not detect the tail recursion? I think I crafted it after their guide, but perhaps it has changed since.
Emilio Jesús Gallego Arias (May 08 2021 at 21:46):I was talking about the code in Coq's upstream, not the one we ship
Emilio Jesús Gallego Arias (May 08 2021 at 21:47):the code was replaced but in similar spirit
Shachar Itzhaky (May 08 2021 at 21:48):Oh. So why does cps.patch not fix that?
I have tried a local build with debug but so far has not been able to reproduce the bug in 8.13.0; trying a fresh build.
Shachar Itzhaky (May 08 2021 at 21:48):(The version on the website is from a Docker build)
Emilio Jesús Gallego Arias (May 08 2021 at 21:48):Maybe the patch didn't apply for some reason?
Shachar Itzhaky (May 08 2021 at 21:48):I checked the output, there is no error message regarding the patch.
Shachar Itzhaky (May 08 2021 at 21:49):I really should run my Docker in such a way that the logs are stored for future inspection.
Emilio Jesús Gallego Arias (May 08 2021 at 21:51):All stuff that it is jit related is very tricky in general
Emilio Jesús Gallego Arias (May 08 2021 at 21:51)::S
Shachar Itzhaky (May 08 2021 at 21:53):Ooh I wonder if it has anything to do with the OPAM anomaly where elpi caused it to downgrade to jsoo 3.7.1. It would actually build jscoq with 3.9.0 and mathcomp with 3.7.1 as a result (since mathcomp comes after elpi in the pipline...).
Shachar Itzhaky (May 08 2021 at 21:53):My local build would have done the same tho. So still confused.
Shachar Itzhaky (May 08 2021 at 22:08):Oh it happens in regular build but not in a debug build. But of course :face_palm:
Emilio Jesús Gallego Arias (May 09 2021 at 00:08)::dragon_face:
Last updated: May 31 2023 at 02:31 UTC