Peter Gumm (Feb 10 2023 at 15:27): Peter Gumm (Feb 10 2023 at 15:27):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.
Huỳnh Trần Khanh (Feb 10 2023 at 16:08):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.
Paolo Giarrusso (Feb 10 2023 at 17:10):@Huỳnh Trần Khanh Have you had success with remoting and VsCoq? I recall otherwise but evidence was limited
Emilio Jesús Gallego Arias (Feb 10 2023 at 17:10):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
Emilio Jesús Gallego Arias (Feb 10 2023 at 17:11):the standalone version in the browser will have the choice to connect it to a git backend
Emilio Jesús Gallego Arias (Feb 10 2023 at 17:14):Note that Ctrl-O / Ctrl-S only work in the scratchpad
Emilio Jesús Gallego Arias (Feb 10 2023 at 17:14):https://coq.vercel.app/scratchpad.html
Emilio Jesús Gallego Arias (Feb 10 2023 at 17:14):So indeed they are a bit limited
Peter Gumm (Feb 10 2023 at 22:05):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.
Emilio Jesús Gallego Arias (Feb 11 2023 at 21:53):VsCode will def support the jsCoq rendering mode
Emilio Jesús Gallego Arias (Feb 11 2023 at 21:54):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
Emilio Jesús Gallego Arias (Feb 11 2023 at 21:54):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.
Karl Palmskog (Feb 11 2023 at 21:54):@Emilio Jesús Gallego Arias can we move this to the jsCoq stream?
Emilio Jesús Gallego Arias (Feb 11 2023 at 21:55):I'm unsure how browser-local storage can be made more persistent
Notification Bot (Feb 11 2023 at 21:58):This topic was moved here from #Coq users > jscoq saving and reloading by Karl Palmskog.
Karl Palmskog (Feb 11 2023 at 22:00):if there is any interest in spinning off VsCode related discussion into #VsCoq devs & users or #coq-lsp I can help with that.
Karl Palmskog (Feb 11 2023 at 22:07):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
Emilio Jesús Gallego Arias (Feb 11 2023 at 22:44):Saving / reloading is only for local storage so not optimal
Emilio Jesús Gallego Arias (Feb 11 2023 at 22:45):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
Bas Spitters (Feb 12 2023 at 18:24):@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.
Emilio Jesús Gallego Arias (Feb 12 2023 at 19:29):@Bas Spitters how do students save their progress in your setup?
Bas Spitters (Feb 13 2023 at 09:28):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.
Peter Gumm (Feb 13 2023 at 13:21):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.
Bas Spitters (Feb 13 2023 at 13:41):The user experience with the docker image should be better than for vscode-PVS, as the docker image works on all operating systems.
https://github.com/nasa/vscode-pvs
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:
https://github.com/4ever2/au-fsv22
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.
Karl Palmskog (Feb 13 2023 at 13:43):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.
Karl Palmskog (Feb 13 2023 at 13:45):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)
Emilio Jesús Gallego Arias (Feb 13 2023 at 13:48):Yes @Peter Gumm , I agree with you, it is a pity we don't have proper save support yet.
Emilio Jesús Gallego Arias (Feb 13 2023 at 13:49):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
Peter Gumm (Feb 13 2023 at 13:53):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 ;-).
Emilio Jesús Gallego Arias (Feb 13 2023 at 16:22):Yes, the fancier thing includes saving and loading, actually it could be feasible that it is ready for April
Shachar Itzhaky (Feb 25 2023 at 16:12):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