Stream: jsCoq

Topic: Stack overflow in `Require`


view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (May 08 2021 at 13:32):

There was a patch indeed, but there could be a few things.

view this post on Zulip Emilio Jesús Gallego Arias (May 08 2021 at 13:35):

I don't get a stack overflow tho in chrome

view this post on Zulip Emilio Jesús Gallego Arias (May 08 2021 at 13:36):

so it could be some Safari update?

view this post on Zulip Emilio Jesús Gallego Arias (May 08 2021 at 13:36):

First thing to see if just Require without the import creates the problem

view this post on Zulip Emilio Jesús Gallego Arias (May 08 2021 at 13:37):

if the problem is in require, the code path there is simple

view this post on Zulip 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"

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (May 08 2021 at 14:22):

Let me try with a different chrome version

view this post on Zulip Emilio Jesús Gallego Arias (May 08 2021 at 14:23):

Does removing the import help?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Shachar Itzhaky (May 08 2021 at 16:13):

Ah yes. Both removing the import and re-executing the sentence a second time work.

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 08 2021 at 18:26):

Let me check the Import code just out of curiosity.

view this post on Zulip Emilio Jesús Gallego Arias (May 08 2021 at 18:31):

But indeed you have the patch in master to this code

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 08 2021 at 18:33):

Not sure actually how the version in master will behave with jsoo :S

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 08 2021 at 21:47):

the code was replaced but in similar spirit

view this post on Zulip 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.

view this post on Zulip Shachar Itzhaky (May 08 2021 at 21:48):

(The version on the website is from a Docker build)

view this post on Zulip Emilio Jesús Gallego Arias (May 08 2021 at 21:48):

Maybe the patch didn't apply for some reason?

view this post on Zulip Shachar Itzhaky (May 08 2021 at 21:48):

I checked the output, there is no error message regarding the patch.

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (May 08 2021 at 21:51):

All stuff that it is jit related is very tricky in general

view this post on Zulip Emilio Jesús Gallego Arias (May 08 2021 at 21:51):

:S

view this post on Zulip 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...).

view this post on Zulip Shachar Itzhaky (May 08 2021 at 21:53):

My local build would have done the same tho. So still confused.

view this post on Zulip 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:

view this post on Zulip Emilio Jesús Gallego Arias (May 09 2021 at 00:08):

:dragon_face:


Last updated: Mar 28 2024 at 22:01 UTC