Hi, i am exploring whether using Coq in my class on Verification next semester is an option. I like jscoq, since we do not waste time on installation issues. However, saving and reloading files does not work as expected. I am using jscoq als obtained from
https://coq.vercel.app. This lets me work in the nicely rendered HTML-code of the Software Foundation series. Unfortunately, saving and reloading using Ctrl-s and Ctrl-o does not work as expected.
There must be a way to fix this, but so far I could not find it.
Codespaces and Gitpod are two viable options. Ctrl+S and Ctrl+O can't work in jsCoq yet, unfortunately.
Another option: I hope that installing VS Code should be easy for everyone. Then you can grab a spare server, divide it into many containers and install Coq on those containers. Community members made this repo to make things easier for you. And students can use the Remote - SSH extension to connect VS Code to their containers. Then we can use VsCoq.
Disclaimer: I'm not an expert and this should not be construed as expert advice. While I believe the options I provided are useful, your circumstances might differ and I might be completely wrong. I can't guarantee the information I provided is correct.
@Huỳnh Trần Khanh Have you had success with remoting and VsCoq? I recall otherwise but evidence was limited
Hi @Peter Gumm , I'm unsure about the status of the save and open functionality, I cc @Shachar Itzhaky as he may know more about it.
We are very close to releasing jsCoq 2 tho that could help a lot in your case; in particular it features a unified architecture with coq-lsp, so indeed, you can run it standadonle in the browser, in vscode.dev / github.dev, or locally in vs code
the standalone version in the browser will have the choice to connect it to a git backend
Note that Ctrl-O / Ctrl-S only work in the scratchpad
So indeed they are a bit limited
Hi @Emilio Jesús Gallego Arias, what I like about jscoq is that it beutifully renders the html-version of the SoftwareFoundations books and lets me do the examples and exercises right there. Will that be possible with any of the standalone versions, e.g. CoqIde or VScode?
From earlier experience with the CoqIde, I recall that its editor presented me a text which was ASCII, perhaps with a few Unicode symbols.
VsCode will def support the jsCoq rendering mode
Actually there is a technical reason we went with this plan, as to allow people to keep progress of edition in jsCoq documents, in the sense that now they are backed by some full-text format
Before the doc structure was a bit more ad-hoc, even so still I think that jsCoq SF version will save progress, but only locally.
@Emilio Jesús Gallego Arias can we move this to the jsCoq stream?
I'm unsure how browser-local storage can be made more persistent
This topic was moved here from #Coq users > jscoq saving and reloading by Karl Palmskog.
if there is any interest in spinning off VsCode related discussion into #VsCoq devs & users or #coq-lsp I can help with that.
for teaching with jsCoq, might be worth flagging up this which has some specific automation (but not saving/reloading yet I guess): https://github.com/gares/math-comp-school-2022
Saving / reloading is only for local storage so not optimal
Could be implemented tho not too hardly if anyone is interested, we just moved to slightly different model where the source files are rich directly
@Peter Gumm I've been using jscoq for my teaching for a couple of years now, and it works for me.
I also have a docker image that contains all the relevant files, and can easily be called from vscode.
We've been working with the SF team to make this more widely available.
@Bas Spitters how do students save their progress in your setup?
I'm using jscoq for the lectures only. The students install the docker image in use vscode. They hand in via github classroom. We run the SF autograder when they and in, and do manual code review via github after.
Thanks @Bas Spitters , the trouble is just that I actually only know superficially what a docker image is, nor am I familiar with "github.dev" or "vs-code.dev" etc.. At my age (my PhD is from 1977) I am not motivated enough to learn the latest developer tools, only for running a prover like coq, lean or PVS.
The jscoq system from coq.vercel.app with its built-in support for the "Software Foundations" struck me as wonderfully easy and esthetical out of the box, that I considered using it in my class on verification. Alas, without loading and saving, it is unfit for this purpose - which I find very regrettable.
In earlier versions of my course I have used "lean in the browser" and "vscode-PVS" and I would like to try Coq this time. Regarding VS-Coq, I tried two extensions, one is "coq v0.3.2" by "ruoz" and "VSCoq" v0.3.7 by "Maxim Denes" but for my very modest purposes their added value over CoqIde did not jump at me.
The user experience with the docker image should be better than for vscode-PVS, as the docker image works on all operating systems.
All our master students certainly are familiar with docker and vscode, and I expect this generally to be the case for CS students.
Installation is just a matter of following the simple steps here:
which are now also included in the private SF-dev repo: https://github.com/DeepSpec/sfdev/tree/master/extras
@Steve Zdancewic what was your experience running the course at UPenn?
With a bit of work it should also be possible to use the (paid) github code spaces.
I believe @Emilio Jesús Gallego Arias may be planning to to bundle Coq with the coq-lsp extension for vscode.
familiary with (tools like) Docker highly depends on curriculum and personal interest of students. I can say that for 3-4th year CS students at my university, it's quite common, but for 1-2nd year, not so common.
the instructions in the au-fsv22 repo linked by Bas seem fairly straightforward to follow. But downside is that everyone must use the same UI (not always popular)
Yes @Peter Gumm , I agree with you, it is a pity we don't have proper save support yet.
We are doing a fancier thing for jscoq 2 , but I think if someone is interested I could guide them to do a thing that would work out of the box in the current setup
does that "fancier thing" in jscoq include saving and loading? When do you expect jscoq 2 to be out? My course will start Mid April ;-).
Yes, the fancier thing includes saving and loading, actually it could be feasible that it is ready for April
Also we have a pending plan for being able to support local-storage for literate documents such as the SF pages. There are some UX issues because the book also changes occasionally (albeit not very frequently), at which point it is unclear what to do with stored edits. Suggestions welcome!
Last updated: Jun 04 2023 at 23:30 UTC