Coq/Rocq tutorial and practice

Stream: LFTCM 2024

[Cyril Cohen]

Dear participants, the supporting material is located here:
https://github.com/CohenCyril/LFTCM2024_Rocq
There should be no need to prepare in advance as we plan to let you follow using an online version of vscode inside "codespaces".
Should you use the local version, we also documented how to, but you might have to do a git pull tomorrow morning :wink:
(NB: none of these methods provide a system-wide installation of Coq/Rocq, but you are welcome to do so.)

[Vincent Beffara]

For the local version IIUC you also need to have Docker installed and running?

[Cyril Cohen]

Vincent Beffara said:

For the local version IIUC you also need to have Docker installed and running?

That's correct, though vscode is supposed to suggest it, doesn't it?

[Notification Bot]

11 messages were moved from this topic to #LFTCM 2024 > Coq/Rocq tutorial and practice, troubleshooting with M2 mac by Cyril Cohen.

[Cyril Cohen]

In case of trouble installing you can ask here:
https://leanprover.zulipchat.com/#narrow/stream/429416-LFTCM-2024/topic/Coq.2FRocq.20tutorial.20and.20practice.2C.20general.20troubleshooting
and we will do our best to answer

[Florent Schaffhauser]

Great talk by @Marie Kerjean ! Should we open different threads for each Lemma or do all Rocq Preactice here?

[Notification Bot]

2 messages were moved from this topic to #LFTCM 2024 > Coq/Rocq: divand by Cyril Cohen.