Stream: Teaching [with] Coq

Topic: Build systems for teaching


view this post on Zulip Karl Palmskog (Sep 13 2023 at 13:59):

Inspired by this topic, maybe would make sense to look at "Coq build systems for teaching". The only build system I know that should be completely cross-platform is the one built into ProofGeneral

view this post on Zulip Ralf Jung (Sep 13 2023 at 14:00):

how does the installation for that work on windows? you somehow need emacs and then PG in emacs and then link that up with the coq binary?

view this post on Zulip Karl Palmskog (Sep 13 2023 at 14:01):

I didn't try personally, but there is an Emacs build for Windows without any Unix deps. That build works fine with MELPA/ELPA where PG can be found

view this post on Zulip Karl Palmskog (Sep 13 2023 at 14:02):

the problem is likely the path to Coq, yes, but that can be configured in .emacs. Students often do not like Emacs though

view this post on Zulip Ralf Jung (Sep 13 2023 at 14:02):

sounds like the first 2 weeks are spent to teach students emacs and then it's 4 weeks of teaching them coq and then the main course content can start... ;)

view this post on Zulip Ralf Jung (Sep 13 2023 at 14:03):

yeah emacs is a roadblock probably, though I'm concerned they wont like coqide much either. its not exactly on par with modern editors.

view this post on Zulip Ralf Jung (Sep 13 2023 at 14:04):

like, ideally coq-platform would ship with a fully configured vscode where the coq plugin is set up and just works (and supports multi-file projects)... that's my dream world ;)

view this post on Zulip Emilio Jesús Gallego Arias (Sep 13 2023 at 14:05):

jsCoq 1 included a prototype build system done by @Shachar Itzhaky , now jsCoq 2 and coq-lsp will soon include their own build system based in dune

view this post on Zulip Karl Palmskog (Sep 13 2023 at 14:07):

I think the experience with WSL2 + [VS Code on Windows] via remote extension is nice: https://github.com/runtimeverification/vlsm/blob/master/BUILDING.md

view this post on Zulip Pierre Rousselin (Sep 13 2023 at 14:24):

coqide works fine for me with undergraduate students, it's very simple. I might try jscoq

view this post on Zulip Ralf Jung (Sep 13 2023 at 14:31):

Pierre Rousselin said:

coqide works fine for me with undergraduate students, it's very simple. I might try jscoq

do you have any multi-file projects, where one file needs to import another?

view this post on Zulip Pierre Rousselin (Sep 13 2023 at 14:32):

No, I admit... But with a _CoqProject it should work fine, I guess?

view this post on Zulip Ralf Jung (Sep 13 2023 at 14:36):

no, coqide cant build files you import

view this post on Zulip Ralf Jung (Sep 13 2023 at 14:36):

you need to somehow get the .vo files

view this post on Zulip Ralf Jung (Sep 13 2023 at 14:37):

are .vo files portable? like, can we generate them with coq 8.17.1 on linux and then ship them to windows users with that exact same coq version? (yeah Im getting a bit desperate^^)

view this post on Zulip Gaëtan Gilbert (Sep 13 2023 at 14:38):

I think you would need to ship the stdlib with them, otherwise it will do the usual inconsistent assumptions error

view this post on Zulip Karl Palmskog (Sep 13 2023 at 14:39):

.vo files are tied to the OCaml compiler that produced them (is my understanding of OCaml's Marshal)

One option for you might be to produce a custom Coq Platform Windows installer with all .vo files students will use, then have them only edit/check a single file

view this post on Zulip Karl Palmskog (Sep 13 2023 at 14:39):

https://github.com/coq/platform/blob/main/doc/FAQ-customized-installers.md

view this post on Zulip Pierre Rousselin (Sep 13 2023 at 14:43):

Ralf Jung said:

you need to somehow get the .vo files

So your problem is with building .vo files on Windows, if I understand correctly?

view this post on Zulip Pierre Rousselin (Sep 13 2023 at 14:44):

This issue has probably been encountered by the software foundations people.

view this post on Zulip Ralf Jung (Sep 13 2023 at 14:54):

Karl Palmskog said:

.vo files are tied to the OCaml compiler that produced them (is my understanding of OCaml's Marshal)

One option for you might be to produce a custom Coq Platform Windows installer with all .vo files students will use, then have them only edit/check a single file

I dont think that will work, students will have to edit files and import edited files.

view this post on Zulip Ralf Jung (Sep 13 2023 at 14:54):

Pierre Rousselin said:

Ralf Jung said:

you need to somehow get the .vo files

So your problem is with building .vo files on Windows, if I understand correctly?

my problem is that when you open the 2nd file in coqide and ask it to jump into the proof it says that it cannot import the first file

view this post on Zulip Ralf Jung (Sep 13 2023 at 14:55):

because something needs to build that .vo file. ideally that would happen transparently of course; on Linux/macOS we can use make by hand to work around that, on windows we can... make people suffer through the cygwin installer and then use make by hand, it seems.

view this post on Zulip Pierre Rousselin (Sep 13 2023 at 15:02):

This needs to be addressed, you are right... Indeed a WSL-based solution could work, but it would probably be better if it is handled directly by the IDE.

view this post on Zulip Ralf Jung (Sep 13 2023 at 15:26):

with WSL we need two coq installations, one in WSL and one on the host for coqide

view this post on Zulip Ralf Jung (Sep 13 2023 at 15:26):

or we run coqide inside WSL, but then we need a coq-platform-in-WSL installer...

view this post on Zulip Ralf Jung (Sep 13 2023 at 15:27):

for now we're going to try to use cygwin. the official cygwin installer is a total nightmare but the script in the coq platform seems to work pretty well and we might just take that script and adjust it a bit to remove the parts we dont need...

view this post on Zulip Paolo Giarrusso (Sep 13 2023 at 16:29):

Ralf: coq-lsp integrates a simple build system

view this post on Zulip Paolo Giarrusso (Sep 13 2023 at 16:30):

Otherwise, you might need a better version of https://github.com/coq-community/vscoq/pull/319 + integration — but I wouldn't push that MR on students

view this post on Zulip Paolo Giarrusso (Sep 13 2023 at 16:30):

also I heard you don't like dune, but I understand it can be installed on Windows without Cygwin

view this post on Zulip Paolo Giarrusso (Sep 13 2023 at 16:34):

are .vo files portable? like, can we generate them with coq 8.17.1 on linux and then ship them to windows users with that exact same coq version? (yeah Im getting a bit desperate^^)

Not remotely: they embed hashes of dependencies, and Coq lacks reproducible builds (there's a GitHub ticket). IME rebuilding the same sources but reusing .vos almost ensures inconsistent assumptions errors (on large enough codebases)

view this post on Zulip Paolo Giarrusso (Sep 13 2023 at 16:35):

coq-platform-in-WSL installer...

That's just the Linux installer.

view this post on Zulip Ralf Jung (Sep 14 2023 at 09:25):

the linux installer is a snap package. snap in WSL seems to be highly experimental at best.

view this post on Zulip Ralf Jung (Sep 14 2023 at 09:26):

Paolo Giarrusso said:

Ralf: coq-lsp integrates a simple build system

ah, did that change? last time I tried the vscode integration I couldnt find anything. something to consider for the next semester I guess. (or maybe during the semester, if we get enough complaints.^^)

view this post on Zulip Ralf Jung (Sep 14 2023 at 09:27):

(deleted)

view this post on Zulip Pierre Rousselin (Sep 14 2023 at 09:35):

I will try it out at home (I still have windows 10 on a machine). This needs to be addressed before any serious pedagogical discussions.

view this post on Zulip Paolo Giarrusso (Sep 14 2023 at 09:57):

Ralf: there kinda are three Coq vscode plugins: vscoq1 (coqide-like), vscoq2 (needs coq 8.18) and coq-lsp (more experimental? maybe also works with 8.17)

view this post on Zulip Paolo Giarrusso (Sep 14 2023 at 09:58):

Vscoq2 is a rewrite of vscoq1, and coq-lsp makes different decisions

view this post on Zulip Ralf Jung (Sep 14 2023 at 09:59):

three? :(

view this post on Zulip Paolo Giarrusso (Sep 14 2023 at 10:00):

Vscoq1 is legacy, but still needed for old Coq

view this post on Zulip Michael Soegtrop (Sep 14 2023 at 10:39):

@Ralf Jung : again: if you need a more complete development environment on Windows, I would recommend cygwin. The setup of Coq via cygwin is highly automated and battle proven (in CI and several courses). You run a single command (after expanding a Coq platform scripts ZIP) and that's it. Installing WSL has a rather deep impact on a system and a lot of odd things can happen (I had my share of it). By contrast Installing cygwin doesn't do anything to your computer besides the files in the destination folder and 2 or 3 start menu shortcuts.

view this post on Zulip Ralf Jung (Sep 14 2023 at 11:26):

yeah currently we are leaning towards copying and adjusting your platform batch script to install enough of cygwin for things to work

view this post on Zulip Ralf Jung (Sep 14 2023 at 11:26):

so basically people will install the binary distribution of the platform for coqide, coqc, and the dependencies; and run that script for make (and the unix utilities required for the makefile)

view this post on Zulip Ralf Jung (Sep 14 2023 at 11:28):

I know cygwin paths can be problematic etc but when we tried this it worked good enough to run make and that's really all we need :shrug:

view this post on Zulip Michael Soegtrop (Sep 14 2023 at 11:49):

OK. as discussed in PC, an alternative would be a simple WIndows native solution based on coqmakefile + remake and possibly some 10 lines of C. But I think one can patch the templates of coqmakefile such that remake can handle the result with CMD as shell - and remake is trivial to supply on Windows.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 14 2023 at 15:24):

coq-lsp does also work on windows from the native Shell, so that's quite an improvement for some. Indeed, our goal is to solve soon all the problems @Ralf Jung have found in teaching.

view this post on Zulip Michael Soegtrop (Sep 14 2023 at 15:25):

@Emilio Jesús Gallego Arias : do you know how the status of dune not requiring ocamlc at run time is?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 14 2023 at 15:26):

@Michael Soegtrop there has been some progress on that, but still not released. Note tho that coq-lsp doesn't have this restriction.

view this post on Zulip Michael Soegtrop (Sep 14 2023 at 16:42):

@Emilio Jesús Gallego Arias : I am confused - I thought coq-lsp is "just" a language server. Can it build projects?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 14 2023 at 16:47):

@Michael Soegtrop , yes, language servers can have this capability. In fact for Coq is very important, otherwise the current .vo model is very limited. I know things are a bit confusing, we are trying to improve the README, under the coq-lsp repos we have:

view this post on Zulip Ralf Jung (Sep 15 2023 at 07:08):

@Emilio Jesús Gallego Arias how does coq-lsp relate to vscoq2? Seeing our very sparse developer resources spread thin across multiple vscode plugins is quite concerning.

view this post on Zulip Karl Palmskog (Sep 15 2023 at 07:09):

standard answer: coq-lsp is a research project, VsCoq2 is not

view this post on Zulip Ralf Jung (Sep 15 2023 at 07:10):

hm, I dont understand what this means for users

view this post on Zulip Karl Palmskog (Sep 15 2023 at 07:11):

VsCoq2 is developed mainly by @Romain Tetley, an Inria research engineer who works with long-term backing from Inria

view this post on Zulip Ralf Jung (Sep 15 2023 at 07:12):

right... but as a user of either that means what? how do I decide which one to use? as a user I care little about the mode of development. I care about stability, maturity, features covered, ...

view this post on Zulip Karl Palmskog (Sep 15 2023 at 07:14):

obviously the mode of development is a guide to what will be prioritized

view this post on Zulip Ralf Jung (Sep 15 2023 at 07:16):

I dont have a crystal ball so I cannot deduce from this information what the developers will prioritize

view this post on Zulip Ralf Jung (Sep 15 2023 at 07:16):

but it does seem like they are completely independent projects then and a lot of duplicated effort. :(

view this post on Zulip Ralf Jung (Sep 15 2023 at 07:17):

coq-lsp mentions opam in its installation instructions so that's already basically a no-go for teaching I think...^^ I guess it could eventually be packaged in the platform or so to avoid that issue?

view this post on Zulip Karl Palmskog (Sep 15 2023 at 07:25):

https://github.com/coq/platform/issues/319

view this post on Zulip Emilio Jesús Gallego Arias (Sep 15 2023 at 09:02):

Indeed I tried to put coq-lsp in the platform but I'm unsure how to make that progress. Any help with that is very welcome, especially as coq-lsp has good windows support.

@Ralf Jung your other concerns are very valid and I share them.

view this post on Zulip Michael Soegtrop (Sep 15 2023 at 09:16):

@Emilio Jesús Gallego Arias : as discussed offline coq-lsp was too late for the 2023.03 release and is planned for the 2023.09 release, which we started to build last week, but it will take 6..8 weeks. If coq-lsp is critically important, we can make a 2023.08.1 release, but building and signing the installers is a lengthy process, so it won't be in time for Ralf.

view this post on Zulip Michael Soegtrop (Sep 15 2023 at 09:16):

@Ralf Jung : as discussed I am working on a solution - we should concentrate on that.

view this post on Zulip Ralf Jung (Sep 15 2023 at 09:21):

yeah I wasnt planning on using vscode for the course anyway

view this post on Zulip Ralf Jung (Sep 15 2023 at 09:21):

CoqIDE is at least an IDE that I know how to use with Coq

view this post on Zulip Ralf Jung (Sep 15 2023 at 09:21):

vsocde is a good option to keep in mind for next fall :)

view this post on Zulip Michael Soegtrop (Sep 15 2023 at 09:30):

I guess CoqIDE is very vintage to computer science students, but then vintage is "in" these days - you just have to sell it that way ;-)

view this post on Zulip Emilio Jesús Gallego Arias (Sep 15 2023 at 10:12):

Karl Palmskog said:

standard answer: coq-lsp is a research project, VsCoq2 is not

I'm unsure what "being a research project" means; coq-lsp is both a research project and something intended to be used widely by industrial and educational users; there are a lot of differences between both projects in terms of features, implementation, and development methodologies too.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 15 2023 at 10:13):

@Ralf Jung jscoq could be an option for you too

view this post on Zulip Emilio Jesús Gallego Arias (Sep 15 2023 at 10:13):

See the teaching topic for a template.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 15 2023 at 10:14):

Michael Soegtrop said:

Emilio Jesús Gallego Arias : as discussed offline coq-lsp was too late for the 2023.03 release and is planned for the 2023.09 release, which we started to build last week, but it will take 6..8 weeks. If coq-lsp is critically important, we can make a 2023.08.1 release, but building and signing the installers is a lengthy process, so it won't be in time for Ralf.

Sure, for 2023.03 was too late, what I mean is that I don't understand what I need to do in terms of pull requests / code.

I'm happy to help with making a new release etc... but I need to get the package building in the CI first, this is the step I'm lost.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 15 2023 at 10:17):

I'd be happy even with an unsigned installer, I understand that there are some large teaching courses that intend to use coq-lsp this fall, and it works well for them, but they are distributing their own binaries to students which is a large load.

So if we can figure out how to build an unsigned installer that includes coq-lsp, we'd be happy to do the integration and testing work, so it is ready for the next release; also students can install an interim build easily.

view this post on Zulip Ralf Jung (Sep 15 2023 at 10:23):

Emilio Jesús Gallego Arias said:

Ralf Jung jscoq could be an option for you too

last time I tried it it was way too slow for practical use. but that was many years ago.
does it support multi-file workspaces and all that? students need to have persistent data -- work on their files, save, get back to it.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 15 2023 at 10:33):

@Ralf Jung jsCoq 2.0 will support multi-file workspaces, as it is based on Flèche, but that won't ready until end-of-year I think, maybe sooner.

jsCoq "1.0" does support a single file, the support for multiple files that Shachar did I think is still a bit experimental.

So in jsCoq "1.0" you need to structure the classes in several html files, and have each file load the completed previous file.

It is a bit messy; thankfully the newer version is much better.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 15 2023 at 10:33):

So it depends on your needs / calendar

view this post on Zulip Ralf Jung (Sep 15 2023 at 11:11):

yeah that won't work

view this post on Zulip Ralf Jung (Sep 15 2023 at 11:11):

(I'm also generally not a big fan of cloud-based solutions)

view this post on Zulip Sebastian Ertel (Sep 15 2023 at 11:20):

Hi there,
I use a Nix flake that can be extended to install (spac)emacs and all necessary proof general packages automatically.
The students would only need to install nix and then do a nix develop.
Would that be an option for you?

view this post on Zulip Ralf Jung (Sep 15 2023 at 11:26):

does nix work on Windows? ;)

view this post on Zulip Sebastian Ertel (Sep 15 2023 at 11:31):

WSL? ;)

view this post on Zulip Ralf Jung (Sep 15 2023 at 11:33):

might work^^ and macOS?

view this post on Zulip Ralf Jung (Sep 15 2023 at 11:33):

also from all I heard about nix, you need someone with nix experience on the team

view this post on Zulip Sebastian Ertel (Sep 15 2023 at 11:33):

I use macOS and it works like a charm.

view this post on Zulip Ralf Jung (Sep 15 2023 at 11:33):

so... the coq platform installer sounds a lot more appealing (even though Im not much of a snapd fan)

view this post on Zulip Emilio Jesús Gallego Arias (Sep 15 2023 at 12:11):

Ralf Jung said:

(I'm also generally not a big fan of cloud-based solutions)

There is no cloud in jsCoq, it is just a bunch of html + js that you can run locally, or in a static web-server

view this post on Zulip Emilio Jesús Gallego Arias (Sep 15 2023 at 12:12):

I think Coq Platform should work pretty well Ralf!

view this post on Zulip Ralf Jung (Sep 15 2023 at 13:31):

Emilio Jesús Gallego Arias said:

I think Coq Platform should work pretty well Ralf!

we'll see :D

view this post on Zulip Ralf Jung (Sep 15 2023 at 13:31):

I am certainly super happy that it exists

view this post on Zulip Ralf Jung (Sep 15 2023 at 13:31):

things would be a lot harder without it

view this post on Zulip Pierre Rousselin (Sep 18 2023 at 11:30):

I've tried using opam on WSL2 and so far it has been inconclusive, no idea why (coq-stdlib would not build). I will try again during the week with different methods.

view this post on Zulip Karl Palmskog (Sep 18 2023 at 11:31):

hmm, coq-stdlib has worked for me thus far in WSL2, but obviously the installation of the gmp system package via depext must succeed.

view this post on Zulip Pierre Roux (Sep 18 2023 at 11:32):

This should work (i.e., I personally never encountered any issue).

view this post on Zulip Pierre Rousselin (Sep 18 2023 at 11:32):

Sorry I don't understand gmp and depext.

view this post on Zulip Karl Palmskog (Sep 18 2023 at 11:34):

coq-core/coq-stdlib depends on package zarith, and zarith depends on conf-gmp. gmp is a system package that can't be installed by opam directly (hinted at by the conf-). However, opam has a built-in system called depext that helps people install system libraries.

view this post on Zulip Karl Palmskog (Sep 18 2023 at 11:34):

the depext approach can work great or fail completely, depending on a number of factors

view this post on Zulip Karl Palmskog (Sep 18 2023 at 11:36):

on Ubuntu/WSL2, the system package is called libgmp-dev. So one thing to test is to manually run sudo apt install libgmp-dev before trying to install coq-core/coq-stdlib

view this post on Zulip Pierre Rousselin (Sep 18 2023 at 11:36):

There was no error message, except the fact that dune was killed.

view this post on Zulip Karl Palmskog (Sep 18 2023 at 11:36):

another possible issue is that you run out of memory for WSL2

view this post on Zulip Karl Palmskog (Sep 18 2023 at 11:37):

I think by default it only uses 50% or something out of your system memory. I never had problems on a 16GB memory machine, but I can imagine an 8GB machine quickly runs out inside WSL2

view this post on Zulip Pierre Rousselin (Sep 18 2023 at 11:38):

It's actually possible since one of my memory card died and I'm on 8GB, though I would be surprised one can play diablo IV and cannot install Coq :D

view this post on Zulip Karl Palmskog (Sep 18 2023 at 11:40):

8GB at Windows level should work fine for Coq-in-Windows and lots of demanding games. But WSL2 cuts this by quite a lot, you can run top inside WSL2 and it should show 4GB or similar

view this post on Zulip Pierre Rousselin (Sep 18 2023 at 11:41):

Thanks! I will do this for documentation purposes (not at home at the moment).

view this post on Zulip Karl Palmskog (Sep 18 2023 at 11:43):

apparently the memory for WSL2 can be adjusted upwards: https://learn.microsoft.com/en-us/windows/wsl/wsl-config#configuration-setting-for-wslconfig

50% of total memory on Windows or 8GB, whichever is less

view this post on Zulip Michael Soegtrop (Sep 18 2023 at 16:39):

I just wanted to mention that the Coq Platform releases 2022.09.1 and 2023.03.0 contain an Addon zip file, which contains preliminary work on running coq_makefile and gnumake with CMD as shell. It does by far not support all features of coq_makefile yet, but the basic build rule for .vo files, Coq dependency file generation and the clean target work. For most lectures this should be good enough. This is delivered as ZIP file with two files (gnumake.exe and a patched template for coq_maefile) which are intended to copied over an installer generated installation. The plan is to integrate this in the next release.

view this post on Zulip Michael Soegtrop (Sep 18 2023 at 16:42):

So for plain Coq lectures, the Coq Platform installers should be fine now on all platform. For lectures also requiring OCaml, the compile from sources Coq Platform is recommended - possibly with a lecture specific pick.

view this post on Zulip Michael Soegtrop (Sep 18 2023 at 16:47):

Regarding WSL2: I would not use it for lectures. In my experience the average install effort is quite high and it has the problem that it does not work very well with other hypervisors. If people have VMware or VirtualBox installed, it might be substantial effort to get these working again. Besides I have seen quite a few strange things with WSL2, say blue screens not working any more (redirected to the hypervisor and ignored there). Also memory consumption can be an issue on laptops (half of 8 GB is quite on the edge for Coq work). IMHO WSL2 is fine for advanced personal work, but I would not ask 100 people to install it.

view this post on Zulip Ralf Jung (Sep 18 2023 at 16:51):

A huge thank you :heart: to @Michael Soegtrop for building this addon package on such short notice, this will be a great help. :)

view this post on Zulip Michael Soegtrop (Sep 18 2023 at 16:53):

My pleasure :-)

view this post on Zulip Pierre Rousselin (Sep 23 2023 at 09:12):

Some feedback on windows + WSL + Debian Coq package

  1. I was surprised to see how easy it was to install the default WSL+Ubuntu. Once windows was updated (which, yes, takes ages, this did not change), entering wsl --installin CMD.exe was enough.
  2. I decided to try the Debian package with coqide. This is now Coq 8.15, I think most people can live with that (it has the enhanced Search).
  3. coqidegives annoying warnings, installing gnome-icon-themesolved most of them but I don't know how to solve these
(coqide:15208): dconf-WARNING **: 10:37:22.199: failed to commit changes to dconf: Could not connect: No such file or directory
  1. I also tried vscode on windows. The integration with WSL looks really good. vscoq "legacy" seems to work out of the box.

view this post on Zulip Karl Palmskog (Sep 24 2023 at 12:34):

hmm... my guess would have been that WSL2 + Snap would be preferred over Debian pacakages (not least since Debian packages available on WSL2 would be several years out of date)

view this post on Zulip Pierre Rousselin (Sep 25 2023 at 08:41):

There are certainly advantages for using opam. For new Linux users however, installing distribution packages should be more natural.

view this post on Zulip Théo Zimmermann (Sep 25 2023 at 09:09):

Karl's suggestion above was not using opam (which would mean compiling from sources) but snap (which provides up-to-date prebuilt binaries). Cf. https://snapcraft.io/coq-prover

view this post on Zulip Pierre Rousselin (Sep 25 2023 at 09:14):

Yes, sorry I misread. Will test it this evening.

view this post on Zulip Michael Soegtrop (Sep 25 2023 at 16:40):

@Pierre Rousselin : my main critics on WSL is that if you install it all other VM systems (VMware, VirtualBox, variants of Qemu) stop working and it can be very hard to get them working again (WSL is easier to install than to fully get rid of). I am quite sure that if you ask 100 computer science students to install WSL, at least 10% won't be very grateful for the havoc this does to their working environment. Maybe this improved meanwhile - my latest tests are about 1 year ago. But definitely before you ask students to do this, you should check the interoperability with common VM systems and warn about side effects.

view this post on Zulip Pierre Rousselin (Sep 26 2023 at 14:08):

So finally the students all used wacoq. As an IDE it's incomplete, because the students can only save their snippets, not reload them. We had no problem with compiling or distributing anything yet because the first file was self-sufficient (it's here in french).

There were a couple of bugs, nothing critical, I noticed something like this when moving back and forth inside a proof:

Stm.add called for a different state (333) than the tip: 336.
This is not supported yet, sorry.

I don't think I will go back to CoqIDE because I noticed that the students have read the "comments" a lot more than during the previous editions. This made them really active during the course and some of them actually finished without any help. I really think a "Coq document for teaching" should be more than pure .v. That's the main reason for me for using jscoq or wacoq.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 26 2023 at 14:37):

Thanks for the feedback @Pierre Rousselin !

view this post on Zulip Emilio Jesús Gallego Arias (Sep 26 2023 at 14:40):

Note that we have a preview of jsCoq 2.0 here https://x80.org/rhino-down/ , if you click the "switch" button you can see this idea a bit better, and it also allows saving in a bit of better format

view this post on Zulip Théo Zimmermann (Sep 26 2023 at 14:52):

Thanks for the feedback Pierre! I agree that having more than a v file is certainly a good idea for teaching, and this is the reason why I've tried experimenting with coq-lsp to get the mv file support. This is very similar to what the jsCoq 2.0 demo linked above shows.

view this post on Zulip Pierre Rousselin (Oct 03 2023 at 16:55):

For the moment, jsCoq 1 suits more my needs than jsCoq 2 (in its current state, which if I'm correct should evolve). I like that the students directly have the html formatting of the "comments" and the proofs in code blocks without touching anything.
However, today, there was a need to load previous sessions. This is a real hindrance. It will be even more when I ask them to submit some homeworks.

I would like it a lot if someone could help me with this as I don't think I can teach myself that much of web programming in such a little time.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 03 2023 at 16:57):

Yes that's a real PITA :( actually there could a very simple solution so have some sort of save / load that can be persisted to disk.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 03 2023 at 16:58):

We already have the list of textareas that are used, so it is a one JS line we could generate a file that would contain an array of the raw contents; loading that back should be also trivial.

That should work right @Shachar Itzhaky ?

view this post on Zulip Pierre Rousselin (Oct 10 2023 at 15:00):

New session today. wacoq 16.0.0 does not like Set Printing Parentheses inside a proof.

Anomaly ""Assert_failure vendor/coq/stm/stm.ml:557:4"."
Please report at http://coq.inria.fr/bugs/.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 10 2023 at 15:22):

Yes, unfortunately this bug is known and only fixed in jsCoq 2.0 ; it is due to a Coq bug. There is already an issue in the bug tracker.


Last updated: Oct 13 2024 at 01:02 UTC