Stream: jsCoq

Topic: SF

Bas Spitters (Sep 02 2021 at 08:58):

This is very cool :tada:
https://jscoq.github.io/ext/sf/

Did anyone make a jscoq version of the terse files in SF?

Shachar Itzhaky (Sep 07 2021 at 16:06):

Hi! In fact I did make such a version but did not upload it to the website yet — it has not been tested sufficiently, or at all. Are you interested in trying it?

BTW the most updated version is at https://coq.vercel.app/ext/sf/, which also includes VFA and SLF. The main github.io page already redirects there, but the subdirectories do not, so we should probably fix that.

Bas Spitters (Sep 07 2021 at 16:51):

@Shachar Itzhaky Yes, I'd be happy to test it.

Shachar Itzhaky (Sep 07 2021 at 16:52):

Great to hear -- I will upload a version and let you know. Cheers.

Shachar Itzhaky (Sep 08 2021 at 22:03):

@Bas Spitters I have set up a terse version of LF here: https://coq-next.vercel.app/ext/sf/lf/terse/toc.html

The page alignment is a bit wonky somehow, but it's otherwise operational. One important note: in slides mode, the default in SF is to go forward/backward using the arrow keys. This is awkward when you also have an editor on the slide. So I have changed it to use PgUp/PgDn when jsCoq is enabled. There is still some weird interaction between switching slides and jsCoq's focus when evaluating sentences. I have not figured out a consistent way to handle this, would love to hear what you think.

Bas Spitters (Sep 10 2021 at 13:38):

That's beautiful :love:
One small issue I noticed was that after entering into an interactive session on a slide, when one presses page-down, then the text does not show up at the top of the page. This is easy to fix though by going back and forward.

Shachar Itzhaky (Sep 10 2021 at 18:37):

hmm I have not noticed that, but that is entirely possible. Scrolling is a daunting issue in these interactive documents.

Bas Spitters (Sep 11 2021 at 14:35):

This is so cool !

There's a minor issue with a spoiler here. It's one of the few places where SF actually uses an interactive session to answer a quiz. This would be very useful in general, and probably SF should be changed a little.
https://coq-next.vercel.app/ext/sf/lf/terse/Logic.html#slide-35

Bas Spitters (Sep 11 2021 at 17:47):

This solution which folds the answer is great:
https://coq-next.vercel.app/ext/sf/lf/terse/Logic.html#slide-61

Shachar Itzhaky (Sep 14 2021 at 17:10):

Thanks!

I have uploaded PLF terse as well. I now see what you meant: if the cursor is in the editor area, normal browser scrolling kicks in when PgDn is pressed instead of SF's hooks. This is weird. I will have to debug it in depth.

Bas Spitters (Sep 15 2021 at 06:35):

Do you know what's happening with the spoilers?

Bas Spitters (Sep 15 2021 at 16:14):

@Shachar Itzhaky about the spoilers. I guess the FOLD keyword is not supported.
Would it be hard to add?
https://github.com/DeepSpec/sfdev/blob/master/lf/Logic.v#L864

Shachar Itzhaky (Sep 16 2021 at 12:11):

Thanks for pointing me towards an instance where the spoilers occur. Yes, the FOLD directive is translated into some HTML+JS that controls the folding, but that probably gets lost when inserting the CodeMirror widget because it converts to plain text first. CodeMirror does have a folding plugin; let me see how hard it might be to preserve the folds that way.

Shachar Itzhaky (Sep 16 2021 at 13:27):

Ok seems like in the particular use case of the quiz, the entire snippet is in FOLD. In this case it is easy to hack something to show/hide the CodeMirror. I have done that, will let you check it out soon.

Shachar Itzhaky (Sep 16 2021 at 14:16):

Here, take a look: https://coq-p-wr.vercel.app/ext/sf/lf/terse/Logic.html#slide-35

Bas Spitters (Sep 16 2021 at 14:46):

Very nice. Thanks for fixing that!

Bas Spitters (Sep 19 2021 at 12:50):

@Shachar Itzhaky
https://coq-next.vercel.app/ext/sf/lf/terse/IndProp.html#slide-9

The folded solution does not animate as a Coq script. Not sure whether that's intended.

Shachar Itzhaky (Sep 19 2021 at 17:25):

I was actually on the fence here. It occurs inside a QUIZ environment. I sort of made an executive decision that only top-level snippets become editable and runnable. WDYT?

Bas Spitters (Sep 19 2021 at 18:30):

I don't see a reason not to make them editable. They are easy to skip, and sometimes it is nice to have the opportunity to elaborate a bit on a quiz, in that case runnable code is good.

Shachar Itzhaky (Sep 20 2021 at 14:27):

Alright! That would be an easy change.

Bas Spitters (Oct 02 2021 at 13:31):

There are too many empty lines here:
https://coq.vercel.app/ext/sf/lf/terse/Imp.html#slide-3
Is this a jscoq issue, or an SF issue?

Bas Spitters (Oct 02 2021 at 14:47):

Similarly. Empty line missing here:
https://coq.vercel.app/ext/sf/lf/terse/Imp.html#slide-10

Shachar Itzhaky (Oct 04 2021 at 16:49):

Thanks. This clearly needs some more systematic treatment. There is some ad-hoc logic that transforms the coqdoc-generated HTML back to source code, which is is need of revision (or replacement?). It's good to have a list of such inconsistent locations. I guess accumulating them here is as good a place as any :squid:

Bas Spitters (Oct 09 2021 at 13:19):

BTW. You're including quite a few dependencies when displaying LF,
which appears to be unnecessary. I'm not entirely sure where they come
from, but one could imagine cleaning them up.
Perhaps with Jason's tool for dependency analysis.

Another nit. There are a couple of empty pages here:
https://coq.vercel.app/ext/sf/lf/terse/IndPrinciples.html#slide-3

Bas Spitters (Oct 09 2021 at 19:16):

@Shachar Itzhaky Some more:
https://coq.vercel.app/ext/sf/lf/terse/ImpParser.html#slide-6

https://coq.vercel.app/ext/sf/lf/terse/ImpCEvalFun.html#slide-3
https://coq.vercel.app/ext/sf/lf/terse/ImpCEvalFun.html#slide-4
wants some line breaks

If this is an SF problem that I can fix easily, I can send a PR to the sfdev repo.

Shachar Itzhaky (Oct 09 2021 at 22:35):

@Bas Spitters This week I will make a short doc for how to build your own version of the jsCoq-ified pages, then perhaps we can investigate this together. As for the deps, I'm afraid LF.Basics imports String and that has a world of deps lurking. I did not find any way around that, but I'm open to suggestions.

Bas Spitters (Oct 10 2021 at 08:25):

Great!
About the dpes, I believe I saw real numbers coming by. I don't think they'd be needed.
The load time is not too bad, though, so I'm not sure it's worth the effort.

Shachar Itzhaky (Oct 10 2021 at 13:05):

It's definitely annoying for slow internet connections (like my home ISP bleh). But for consecutive loads it will be cached, so that's only half bad.

Shachar Itzhaky (Oct 10 2021 at 13:06):

jsCoq does use coqdep to determine the dependencies. So the reals are, in fact, needed; unless there is a bug in my coqdep clone.

Emilio Jesús Gallego Arias (Oct 10 2021 at 16:03):

Indeed reals are pulled in by the arithmetic tactics [lia, etc...] which are used in String to do some proofs.

Shachar Itzhaky (Oct 10 2021 at 16:38):

Alright @Bas Spitters, here is a first draft of the instructions:
https://github.com/DeepSpec/sfdev/blob/jscoq-ongoing/docs/jsCoq.md

Bas Spitters (Dec 10 2021 at 11:57):

Quickchick removed the dependency on perl. This was a problem for installation on Windows, it looks like the same problem showed up in jscoq. So, @Shachar Itzhaky this may simplify your experiments. (I'm done with my teaching for this year.)
https://github.com/QuickChick/QuickChick/releases/tag/v1.6.0

Shachar Itzhaky (Dec 10 2021 at 16:05):

Thanks! I believe we got around this in the past because @Emilio Jesús Gallego Arias made a Dune build for QuickChick. The problem I encountered was when trying to compile the QC volume of SF, naturally some of the chapters invoke QuickChick for the purpose of performing some property-based testing, and such invocation involves running ocamlc at some point. I should investigate it some more.

Emilio Jesús Gallego Arias (Dec 10 2021 at 16:05):

Oh indeed having to run OCaml is a problem, tho I hope that in the medium term Coq can provide an API similar to Isabelle's

Emilio Jesús Gallego Arias (Dec 10 2021 at 16:06):

to call managed external processes such as smt's or OCaml

Emilio Jesús Gallego Arias (Dec 10 2021 at 16:06):

jsoo can indeed compile code on the fly and run it, but it is far from trivial :S

Emilio Jesús Gallego Arias (Dec 10 2021 at 16:07):

not so complex on the technical sense, but more like annoying to setup the whole stuff

Shachar Itzhaky (Dec 10 2021 at 16:07):

In the wasm port it is actually not so hard to invoke ocamlc as a subprocess. waCoq already depends on wasi-kernel and I have previously been able to run ocamlc as well as the OCaml REPL on top of it. Here, too, it is mostly a matter of collecting all the ingredients and mixing them up correctly :)

Bas Spitters (Aug 17 2022 at 10:48):

@Shachar Itzhaky Just a heads up. Now versions of the SF books are available now (the QC is coming soon I understand).
You may want to update the corresponding jscoq pages at some point.

Shachar Itzhaky (Aug 17 2022 at 10:49):

Yes I started updating @ coq-next.now.sh/ext/sf, but then I saw that pushes are still being made :) Thanks for the reminder

Last updated: Jun 10 2023 at 06:31 UTC