I would like to introduce my students to Rocq and I was wondering which of the following options you would suggest in order to use Rocq online:
I do not fully understand the difference between 1 and 2 but there must be one because the first app works fine in Firefox but does not seem to work in Safari.
There are also:
0. https://coq-next.vercel.app/
3. https://x80.org/rhino-coq/
I think they are “just” different versions of the same software, sorted from most to least current, specifically running the Rocq versions:
My intuition would be to go with the most current version that runs, but unfortunately all of them are outdated compared to current release Rocq (they even all predate the renaming to Rocq). But for a low-commitment easy introduction to Rocq, having these options is great. I myself had to use them extensively before getting a local Rocq installation working¹ and they basically covered me through the entirety of “Logical Foundations” and some small homework projects, only fully falling short for a multi-file project since I never figured out the file-managing capabilities.
¹ I’d like to emphasize that this does not have to be hard, but my computer situation was euphemistically less than optimal.
(Edit: Actually, I would also guess the “wa” is not only a different version in the sense of a different version number, but also relies on WebAssembly instead of regular JavaScript. Not sure how much of a difference that makes, though.)
Great, thanks! I didn’t know coq-next and it seems that version 8.17.1 works well with Safari too. I’ll follow your recommendation and use that one 
In fact, there is even a Web Assembly version of 8.17.1 at https://coq-next.vercel.app/wa and it seems to be compatible with more browsers than the Javascript version.
When you used this setup, were you mostly using the scratchpad or were you also producing webpages with code, like the one we see under the above link? I think this looks great but I wonder if it is complicated to do.
I was just using the scratchpad, unfortunately, so I cannot point you anywhere helpful on that.
Oh, no worries, I was just curious! I’ll use the scratchpad, too. My plan is to give the students a Rocq file and tell them to copy paste its content into the scratchpad.
A brand new version of JsRocq (2.0, which builds on E. Gallego Arias’ work on rocq-lsp) exists too. Looking around, I found at least two versions of it:
As a disclaimer, Emilio, who was the driving force behind JsRocq has recently changed job, and so the situation with Rocq IDEs, especially browser-based ones, is a bit messy at the moment but should hopefully improve soon!
One can also use a vscode.dev workspace ( Visual Studio Code for the Web ) using the coq-lsp (soon to be rocq-lsp) extension (running the Rocq 9.1.0 version currently). One needs to enable the extension, reload the window and then open a .v file. The hello-rocq devcontainer linked above does it all for you.
Thank you both for the pointers! It is great to know that it is also possible to use Rocq 9 and above in a browser. I see that compilation happens slightly differently, too (no keyboard combination). And saving files to the local disk does not work quite as well yet, it seems.
Anyway, I still have a couple of weeks to decide. I think that a VS Code like interface might be familiar to most, indeed. Similarly, the fact that a GitHub account seems to be required to use Hello-Rocq will most likely not be a problem for the students 