Cody Roux (Feb 03 2021 at 21:56): Cody Roux (Feb 03 2021 at 21:56):I'm getting stackoverflow errors in relatively innocuous proofs in CollaCoq (with about 49 cases). Is there an easy way to increase the stack limit?
Emilio Jesús Gallego Arias (Feb 03 2021 at 22:50):@Cody Roux what browser are you using? Do these Stack Overflows happen if you use the 0.12 version at jscoq.github.io ?
Emilio Jesús Gallego Arias (Feb 03 2021 at 22:51):@Shachar Itzhaky did some improvements so it is possible that indeed updating our installation to a newer version would help; but in the end SO will remain a problem until @Shachar Itzhaky decides to release wacoq [the webassembly version] more publicily [note that we have a jscoq stream in this Zulip by the way]
Cody Roux (Feb 03 2021 at 23:32):Oh, apologies for not using the appropriate stream
Emilio Jesús Gallego Arias (Feb 03 2021 at 23:39):No worries this is also fine, but you may get more eyes in the jsCoq stream tho.
Emilio Jesús Gallego Arias (Feb 03 2021 at 23:39):@Cody Roux post somewhere a reproducible example for the overflow and for sure we'll have a look
Cody Roux (Feb 04 2021 at 01:50):I did try jscoq.github.io and the problem does not appear to manifest. I'm doing a tutorial at FMIE tomorrow, and I'm sure I'll have a well polished example show up then :). I'll try to build a minimal example tomorrow though.
Cody Roux (Feb 04 2021 at 01:50):Thanks for the attention by the way @Emilio Jesús Gallego Arias !
Notification Bot (Feb 04 2021 at 08:43):This topic was moved here from #Coq users > stackoverflow in collacoq by Théo Zimmermann
Emilio Jesús Gallego Arias (Feb 04 2021 at 14:39):@Cody Roux , if the problem doesn't manifest in jscoq.github.io then I wouldn't bother doing an example, as it is likely fixed; I'll try to update collacoq jscoq install ASAP, but indeed that project is a bit artisanal as of today, I think there were some bugs we didn't yet address.
Cody Roux (Feb 04 2021 at 15:18):Sounds good, thanks again!
Shachar Itzhaky (Feb 04 2021 at 20:35):@Emilio Jesús Gallego Arias I started working on extracting the hastebin functionality from Collacoq and including it in core jsCoq UI. It feels more "native" perhaps, as a user may start scribbling on the jsCoq scratchpad then wish to share the result with another user. I will locate the branch where I had this going. :grinning_face_with_smiling_eyes:
Cody Roux (Feb 04 2021 at 21:27):Cool! I think that would be very useful indeed.
Emilio Jesús Gallego Arias (Feb 04 2021 at 21:55):That's cool, maybe we want something more fancy tho
Emilio Jesús Gallego Arias (Feb 04 2021 at 21:56): Cody Roux (Feb 04 2021 at 22:11):Simple is nice! We just did a big tutorial session where people just copy pasted into the buffer.
Emilio Jesús Gallego Arias (Feb 04 2021 at 22:17):@Cody Roux hastebin works pretty well, however it is missing collaborative editing and some other stuff which is IMO important; given that jsCoq is mainly useful as a demo / teaching tool I think in this case it'd be worth it
Emilio Jesús Gallego Arias (Feb 04 2021 at 22:19):For example @Anil Madhavapeddy just tweeted https://twitter.com/avsm/status/1356994468893835270 this which is IMO more in line with what I'd be cool
http://hackmd.io seems to be the breakout dev tool of the year. It's remarkable how good it is to quickly write markdown notes with collaborators while on a video chat, and glue them together into a book. Great job @hackmdio, especially the graphviz/mermaid integration!
- Anil Madhavapeddy (@avsm) Cody Roux (Feb 04 2021 at 22:26):Fair enough.
Last updated: Apr 19 2024 at 11:02 UTC