Stream: jsCoq

Topic: 0.13.0

view this post on Zulip Shachar Itzhaky (May 21 2021 at 20:00):

Almost there — I have made a release page. I am waiting until @Benjamin Pierce announces the new edition of SF, because I have also updated our SF with the May 2021 edition on the website (coq-next.vercel.app/ext/sf).

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

I am getting a strange crash on Chromium and Chrome on Linux. Trying to load waCoq (coq.vercel.app/wa), Chromium reports a memory access error and Chrome crashes. Firefox works fine (and Mac works fine). The problem also seems to disappear if the dev tools are open. So this may be a race condition of some sort? @Emilio Jesús Gallego Arias do you get similar behavior?

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

I get a 404 on that URL @Shachar Itzhaky

view this post on Zulip Shachar Itzhaky (May 22 2021 at 17:20):

Ah yes sorry coq-next.vercel.app/wa...

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2021 at 10:46):

Yup, I get the crash here!

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2021 at 10:46):

Seems like a Chrome bug?

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

I see the sigsev on the official release too :S :S

view this post on Zulip Shachar Itzhaky (Jun 05 2021 at 16:38):

Ok sry I haven't had the chance to debug it. On a Linux VM I didn't get the crash, I will have to debug it on the Linux server... I srsly have no idea where to start.

view this post on Zulip Shachar Itzhaky (Jun 05 2021 at 16:53):

It has to do with the str bindings. Probably easier to debug in Chromium where instead of crashing it throws an exception.

view this post on Zulip Shachar Itzhaky (Jun 11 2021 at 19:24):

@Emilio Jesús Gallego Arias this does not seem to crash for me anymore in Chrome 91.
Chromium 90 still errors, and there isn't a newer version in their package repo.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2021 at 19:59):

Good to hear! Actually I was wondering if the problem we were seeing was due to https://v8.dev/blog/sparkplug , so I indeed went to wait until the refine some glitches this seem to have introduced

view this post on Zulip Shachar Itzhaky (Jun 11 2021 at 20:27):

oh interesting! it does sound like this is purely for the JS part, but clearly a lot had to change in the overall framework to fit this in. I wonder if this bug actually happened only on Linux or maybe I just skipped M90 of Chromium on my Mac so I never experienced it.

Last updated: May 31 2023 at 03:30 UTC