This is very cool :tada:
https://jscoq.github.io/ext/sf/
Did anyone make a jscoq version of the terse files in SF?
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.
@Shachar Itzhaky Yes, I'd be happy to test it.
Great to hear -- I will upload a version and let you know. Cheers.
@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.
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.
hmm I have not noticed that, but that is entirely possible. Scrolling is a daunting issue in these interactive documents.
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
This solution which folds the answer is great:
https://coq-next.vercel.app/ext/sf/lf/terse/Logic.html#slide-61
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.
Do you know what's happening with the spoilers?
@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
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.
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.
Here, take a look: https://coq-p-wr.vercel.app/ext/sf/lf/terse/Logic.html#slide-35
Very nice. Thanks for fixing that!
@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.
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?
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.
Alright! That would be an easy change.
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?
Similarly. Empty line missing here:
https://coq.vercel.app/ext/sf/lf/terse/Imp.html#slide-10
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:
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
@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.
@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.
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.
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.
jsCoq does use coqdep to determine the dependencies. So the reals are, in fact, needed; unless there is a bug in my coqdep clone.
Indeed reals are pulled in by the arithmetic tactics [lia, etc...] which are used in String to do some proofs.
Alright @Bas Spitters, here is a first draft of the instructions:
https://github.com/DeepSpec/sfdev/blob/jscoq-ongoing/docs/jsCoq.md
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
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.
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
to call managed external processes such as smt's or OCaml
jsoo can indeed compile code on the fly and run it, but it is far from trivial :S
not so complex on the technical sense, but more like annoying to setup the whole stuff
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 :)
@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.
Yes I started updating @ coq-next.now.sh/ext/sf, but then I saw that pushes are still being made :) Thanks for the reminder
@Shachar Itzhaky https://softwarefoundations.cis.upenn.edu/ has released a new version.
Do you have time to update jscoq? My teaching starts tomorrow, and it would be convenient to have it. (I'll manage if you don't have time.)
Classes are also starting at UPenn this week.
hi, I was actually planning on doing that today :) I will try to update coq-next, it will be using 8.17 because this is the official SF version now. I assume you can start with the current coq-next -- usually the first chapters are not changed significantly. I will let you know when I have a newer version.
Great! BTW there's also a "new" release of QuickChick v2.0
https://github.com/QuickChick/QuickChick/releases/tag/v2.0
I have not run a thorough test but can you at least verify that this is a usable version?
https://coq-p-wr.vercel.app/ext/sf
BTW I managed to reproduce my working version of ocamlc
on WebAssembly, check it out it's cute
https://basin.vercel.app/
(ignore errors involving tex, they are irrelevant)
Shachar Itzhaky said:
I have not run a thorough test but can you at least verify that this is a usable version?
https://coq-p-wr.vercel.app/ext/sf
How can someone build the same thing for another branch of SF?
oh you are touching a subtle point @grianneau . This can now be done with the jsCoq SDK but I have to upload one for 8.17.
it uses a Docker container to host coqc
and offloads creation of .vo
files to it.
Shachar Itzhaky said:
I have not run a thorough test but can you at least verify that this is a usable version?
https://coq-p-wr.vercel.app/ext/sf
Thanks! Seems to work, at least the Induction chapter of LF.
I see the QC book is not included yet.
no, see the comment above. I managed to get ocamlc
to work again, now I need to stitch it together somehow.
Last updated: Sep 25 2023 at 12:01 UTC