Coq/Rocq tutorial and practice, general troubleshooting

Stream: LFTCM 2024

[Harald Helfgott]

Can you also give a single command that will work for us Linux users?

[Cyril Cohen]

Harald Helfgott said:

Can you also give a single command that will work for us Linux users?

The same should work for linux users, but it should also be handled via vscode and docker as long as you have an amd64 architecture

[Harald Helfgott]

The same should work for linux users, but it should also be handled via vscode and docker as long as you have an amd64 architecture

I'm getting "[WARNING] No package definitions found at
...
Nothing to do"
Presumably I am missing a step?

[Cyril Cohen]

Harald Helfgott said:

The same should work for linux users, but it should also be handled via vscode and docker as long as you have an amd64 architecture

I'm getting "[WARNING] No package definitions found at
...
Nothing to do"
Presumably I am missing a step?

Did you cd to the directory of LFTCM2024_Rocq, and did you do git pull to get the latest version, before you typed the opam command?

[Harald Helfgott]

Ah, I take I must use git again? I didn't get that directory when I pulled LFTCM2024

[Cyril Cohen]

Yes, the Rocq session for tomorrow uses a different repository:
https://github.com/CohenCyril/LFTCM2024_Rocq

[Cyril Cohen]

However, we provide instruction to run it online rather than on your machine.

[Notification Bot]

A message was moved here from #LFTCM 2024 > Coq/Rocq tutorial and practice, troubleshooting with M2 mac by Cyril Cohen.

[Notification Bot]

5 messages were moved here from #LFTCM 2024 > Coq/Rocq tutorial and practice, troubleshooting with M2 mac by Cyril Cohen.

[Notification Bot]

A message was moved here from #LFTCM 2024 > Coq/Rocq tutorial and practice, troubleshooting with M2 mac by Cyril Cohen.