Shachar Itzhaky (Sep 09 2022 at 19:25): 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.
Emilio Jesús Gallego Arias (Sep 09 2022 at 20:54):Looks better and better each release!
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)
Enrico Tassi (Sep 09 2022 at 21:05):in coq_worker.bc.cjs
Karl Palmskog (Sep 09 2022 at 21:05):for me it hung in Firefox but worked in regular Chrome
Enrico Tassi (Sep 09 2022 at 21:06):105.0.5195.52 (Official Build) snap (64-bit)
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 :(
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?
Emilio Jesús Gallego Arias (Sep 09 2022 at 21:07):I always though the problem was that my Chromium is extremely locked down
Emilio Jesús Gallego Arias (Sep 09 2022 at 21:07):as it is my main browser
Emilio Jesús Gallego Arias (Sep 09 2022 at 21:07):gotta try with a new chromium profile without lock down
Enrico Tassi (Sep 09 2022 at 21:08):ffox 104
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 ?
Karl Palmskog (Sep 09 2022 at 21:09):WA version doesn't hang in Firefox (104)
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
Emilio Jesús Gallego Arias (Sep 09 2022 at 21:13):Mmm, that shouldn't happen, does that happen in 8.15?
Enrico Tassi (Sep 09 2022 at 21:14):so, google-chrome works, but elpi fails to load with Not_found :-/
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
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/.
Emilio Jesús Gallego Arias (Sep 09 2022 at 21:25):Elpi should be fixed very soon I understand
Emilio Jesús Gallego Arias (Sep 09 2022 at 21:25):elpi and all the other plugins
Emilio Jesús Gallego Arias (Sep 09 2022 at 21:25):that need findlib
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
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
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
Karl Palmskog (Sep 09 2022 at 21:49):For the record: https://github.com/jscoq/jscoq/issues/291
Emilio Jesús Gallego Arias (Sep 09 2022 at 21:59):Thanks
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!
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.
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.
Shachar Itzhaky (Sep 10 2022 at 15:46):Thanks everyone for testing and 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: Apr 20 2024 at 02:40 UTC