Huỳnh Trần Khanh (Aug 29 2022 at 06:36): 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?
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.
Bas Spitters (Aug 29 2022 at 13:06):Thanks for fixing this. I also tripped over this when teaching my Coq class this morning...
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
Shachar Itzhaky (Aug 29 2022 at 13:10):oh no! they should be working, I will check soon
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.
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.
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: Sep 28 2023 at 09:01 UTC