Stream: jsCoq

Topic: 0.16.0 Preview


view this post on Zulip Shachar Itzhaky (Sep 09 2022 at 19:25):

Preparing for liftoff: Coq 8.16 has been released and jsCoq 0.16.0 is now available for you to test at https://coq-next.now.sh.
Try the new "quick help" screen :stuck_out_tongue: the SF section is also updated and tested.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 09 2022 at 20:54):

Looks better and better each release!

view this post on Zulip Enrico Tassi (Sep 09 2022 at 21:04):

I'm having troubles, it loops with the "Coq ... | world". Inspecting the JC console gives: Uncaught RangeError: Maximum call stack size exceeded
(both ffox and chromium)

view this post on Zulip Enrico Tassi (Sep 09 2022 at 21:05):

in coq_worker.bc.cjs

view this post on Zulip Karl Palmskog (Sep 09 2022 at 21:05):

for me it hung in Firefox but worked in regular Chrome

view this post on Zulip Enrico Tassi (Sep 09 2022 at 21:06):

105.0.5195.52 (Official Build) snap (64-bit)

view this post on Zulip Emilio Jesús Gallego Arias (Sep 09 2022 at 21:06):

@Enrico Tassi for some reason it's been a while Chromium doesn't work for me :(

view this post on Zulip Emilio Jesús Gallego Arias (Sep 09 2022 at 21:06):

I need to use Chrome, not sure what kind of tweak they do, maybe it is time to open an issue?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 09 2022 at 21:07):

I always though the problem was that my Chromium is extremely locked down

view this post on Zulip Emilio Jesús Gallego Arias (Sep 09 2022 at 21:07):

as it is my main browser

view this post on Zulip Emilio Jesús Gallego Arias (Sep 09 2022 at 21:07):

gotta try with a new chromium profile without lock down

view this post on Zulip Enrico Tassi (Sep 09 2022 at 21:08):

ffox 104

view this post on Zulip Emilio Jesús Gallego Arias (Sep 09 2022 at 21:08):

Does the WA version work better https://coq-next.vercel.app/wa/scratchpad.html ?

view this post on Zulip Karl Palmskog (Sep 09 2022 at 21:09):

WA version doesn't hang in Firefox (104)

view this post on Zulip Karl Palmskog (Sep 09 2022 at 21:10):

although if I do forward-backward a couple of times I get the Anomaly "Uncaught exception Stm.Vcs_aux.Expired." which I think has been reported before

view this post on Zulip Emilio Jesús Gallego Arias (Sep 09 2022 at 21:13):

Mmm, that shouldn't happen, does that happen in 8.15?

view this post on Zulip Enrico Tassi (Sep 09 2022 at 21:14):

so, google-chrome works, but elpi fails to load with Not_found :-/

view this post on Zulip Enrico Tassi (Sep 09 2022 at 21:15):

I'd like to see if HB can be used from jscoq, but I guess not yet

view this post on Zulip Enrico Tassi (Sep 09 2022 at 21:16):

wacoq works on ffox, but I get the same error I guess. Although it prints more:
Uncaught exception (Failure
"Config file not found - neither /root/.opamcache/wacoq/lib/findlib.conf nor the directory /root/.opamcache/wacoq/lib/findlib.conf.d")."

Please report at http://coq.inria.fr/bugs/.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 09 2022 at 21:25):

Elpi should be fixed very soon I understand

view this post on Zulip Emilio Jesús Gallego Arias (Sep 09 2022 at 21:25):

elpi and all the other plugins

view this post on Zulip Emilio Jesús Gallego Arias (Sep 09 2022 at 21:25):

that need findlib

view this post on Zulip Karl Palmskog (Sep 09 2022 at 21:43):

Emilio Jesús Gallego Arias said:

Mmm, that shouldn't happen, does that happen in 8.15?

happens both with the WA link and the 8.15 one coq.vercel.app in Firefox 104

view this post on Zulip Karl Palmskog (Sep 09 2022 at 21:45):

I just step up and down randomly in fairly quick suggestion, and I get Uncaught exception Stm.Vcs_aux.Expired. fairly quickly

view this post on Zulip Emilio Jesús Gallego Arias (Sep 09 2022 at 21:45):

@Karl Palmskog if you could submit and issue it'd be appreciated, we use a STM API (newtip) which is indeed buggy for some cases, so maybe that could be related. We could actually add some workaround

view this post on Zulip Karl Palmskog (Sep 09 2022 at 21:49):

For the record: https://github.com/jscoq/jscoq/issues/291

view this post on Zulip Emilio Jesús Gallego Arias (Sep 09 2022 at 21:59):

Thanks

view this post on Zulip Bas Spitters (Sep 10 2022 at 11:46):

Coqoban does not seem to work for me in Brave, but I've never tried it in jscoq before.
SF seems to work.

Thanks for the great work!

view this post on Zulip Shachar Itzhaky (Sep 10 2022 at 12:17):

There seems to be trouble in newer versions with Safari (I don't know if it's a regression in Safari or in jsCoq) that causes the stack overflow at startup in the JS backend. The WA backend works in Safari. I will test Firefox again.

view this post on Zulip Shachar Itzhaky (Sep 10 2022 at 12:19):

Enrico Tassi said:

wacoq works on ffox, but I get the same error I guess. Although it prints more:
Uncaught exception (Failure
"Config file not found - neither /root/.opamcache/wacoq/lib/findlib.conf nor the directory /root/.opamcache/wacoq/lib/findlib.conf.d")."

Please report at http://coq.inria.fr/bugs/.

Yes we are working on it but could not finish it in time for this release — still we wanted to have a version that has 8.16. But I have a prototype that's already working in WA.

view this post on Zulip Shachar Itzhaky (Sep 10 2022 at 15:46):

Thanks everyone for testing reporting the issues! I have addressed the most urgent ones (JS on FF hangs and Coqoban not working :)) and we're working on the others.


Last updated: Jan 31 2023 at 09:01 UTC