Stream: jsCoq

Topic: stackoverflow in collacoq


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

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

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

view this post on Zulip Cody Roux (Feb 03 2021 at 23:32):

Oh, apologies for not using the appropriate stream

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

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

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

view this post on Zulip Cody Roux (Feb 04 2021 at 01:50):

Thanks for the attention by the way @Emilio Jesús Gallego Arias !

view this post on Zulip Notification Bot (Feb 04 2021 at 08:43):

This topic was moved here from #Coq users > stackoverflow in collacoq by Théo Zimmermann

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

view this post on Zulip Cody Roux (Feb 04 2021 at 15:18):

Sounds good, thanks again!

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

view this post on Zulip Cody Roux (Feb 04 2021 at 21:27):

Cool! I think that would be very useful indeed.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2021 at 21:55):

That's cool, maybe we want something more fancy tho

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2021 at 21:56):

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

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

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

view this post on Zulip Cody Roux (Feb 04 2021 at 22:26):

Fair enough.


Last updated: Jun 10 2023 at 06:31 UTC