Erik Martin-Dorel

> Maybe HB 1.9.1 is not compatible with Coq 8.19? we should update the opam package? Certainly, I was thinking about this kind of issue (as an aside, maintaining the...

Thanks for the feedback, BTW it'd be good to understand why, using almost the same versions (in your local switch and in the docker-mathcomp job), HB 1.9.1 fails to build...

Sorry for my vague wording: yes there are no differences, so I'm puzzled that Coq did not find the elpi namespace at that point.

Meanwhile, despite the full-blown renaming, docker-coq only pins the coq package, and docker-rocq only pins the rocq-stdlib, rocq-prover, coqide-server, and I had put the following comment in the Dockerfile: ```...

yes, this pinning is certainly necessary! as https://github.com/LPCIC/coq-elpi/blob/master/coq-elpi.opam doesn't depend on coq, but on coq-core… so if only coq is pinned (not coq-core), bad things happen! :x: ; Thanks again,...

Hi @proux01, I believe all the required building blocks for supporting Coq+Rocq with mathcomp stable and dev are now OK. → I launched the build in docker-base at https://github.com/rocq-community/docker-base/commit/caa184b7d75dc27374bfc11ed82547d960127e54 which...

@pi8027 Nope, I'm really sorry for the delay… this is something I definitely want to look at and fix! it just happens it's the end of the teaching semester, and...

Dear @heades, Good question, it appears the possible teacher workflows are not very well documented currently… (Just tagged your issue as `kind: documentation` BTW.) To sum up, as a teacher...

Also—just to recall—, if you are teacher *and* admin of your learn-ocaml instance, you can also fetch/backup/… the students solutions in the `./sync` subdirectory (or in the typically-mounted-in-a-volume `/sync` directory...

I reopen this issue as it was symptomatic of some incomplete documentation on this topic.