Stream: jsCoq

Topic: Is jsCoq broken?


view this post on Zulip Huỳnh Trần Khanh (Aug 29 2022 at 06:36):

The main page works fine but I used to see a jsCoq editor in the Software Foundations example (https://coq.vercel.app/ext/sf/lf/full/Induction.html) but now the editor is nowhere to be found! Is this a bug?

view this post on Zulip Shachar Itzhaky (Aug 29 2022 at 11:16):

Yes, sorry, I broke the current version of SF because of some silly mishap but the next version (0.16) is up and running and even has a more up-to-date version of the book. https://coq-next.vercel.app/ext/sf/lf/full/Induction.html

Hopefully this will become the default version real soon.

view this post on Zulip Bas Spitters (Aug 29 2022 at 13:06):

Thanks for fixing this. I also tripped over this when teaching my Coq class this morning...

view this post on Zulip Bas Spitters (Aug 29 2022 at 13:09):

@Shachar Itzhaky Looks like the slides are not working. Is that intended?
https://coq-next.vercel.app/ext/sf/lf/terse/Induction.html#slide-8

view this post on Zulip Shachar Itzhaky (Aug 29 2022 at 13:10):

oh no! they should be working, I will check soon

view this post on Zulip Shachar Itzhaky (Aug 30 2022 at 13:32):

Ok. I have rebuilt the terse mode (this was absent from our CI, my bad) and updated coq-next.
The slides seem to malfunction on Safari. But this may have been the case even before.

view this post on Zulip Shachar Itzhaky (Aug 30 2022 at 20:46):

There is some issue (also, not sure if it's new) that pressing pgdn when inside the editor scrolls the browser page instead of forwarding the slide. Pressing pgdn again will get you there; I think this is a byproduct of trying to solve https://github.com/jscoq/jscoq/issues/203. Just be aware of it.

view this post on Zulip Bas Spitters (Sep 01 2022 at 07:48):

Thanks for fixing that!!

Yes, the pgdn issue is known issue. It's slightly surprising at times, but easy enough to work around.


Last updated: Jun 01 2023 at 11:01 UTC