Coq/Rocq tutorial and practice, troubleshooting with M2 mac

Stream: LFTCM 2024

[Vincent Beffara]

Also, the available docker image is for AMD64, on a M2 mac is just eats CPU doing nothing visible

[Vincent Beffara]

Cyril Cohen said:

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?

It didn't suggest it to me, but that might be because I had it installed (but not running) already

[Cyril Cohen]

I am not able to produce something else than amd64 image for now, but I'm looking into it. Unfortunately the coq plateform binaries (which are produced for M2 mac) for the specific set of packages we require in tomorrow session are not yet out (scheduled for April I think). I'm afraid you and all M2 mac users will need to go through codespaces right now. Sorry for the inconvenience

[Florent Schaffhauser]

Oh, good to know, thanks! I was really not understanding the issue on my machine :sweat_smile:

[Vincent Beffara]

I tried to build Coq from the sources and am getting error messages that I don't understand.

Errors:
In environment
x : ?T0
i : ?T3
The term "R" has type "Set" while it is expected to have type "unitRingType".;

(this is line 257 in tutorial.v

[Cyril Cohen]

Vincent Beffara said:

I tried to build Coq from the sources and am getting error messages that I don't understand.

Errors:
In environment
x : ?T0
i : ?T3
The term "R" has type "Set" while it is expected to have type "unitRingType".;

(this is line 257 in tutorial.v

Which version of Coq? You should pick release 8.19.1.
I'm currently crafting an ad-hoc opam package to let you install all the appropriate versions through opam.

[Vincent Beffara]

CP.2023.11.0~8.18~2023.11 is what I was able to install on MacOS

[Cyril Cohen]

Vincent Beffara said:

CP.2023.11.0~8.18~2023.11 is what I was able to install on MacOS

This is the latest version of the Coq Plateform, which does not contain the material we use. Only the future versions will.

[Vincent Beffara]

opam pin add coq 8.19.1 ?

[Vincent Beffara]

I'm just copy pasting commands I'm finding online ...

[Cyril Cohen]

Vincent Beffara said:

I'm just copy pasting commands I'm finding online ...

I know, just give me a few more minutes and I will give you a single command to type :sweat_smile:

[Notification Bot]

11 messages were moved here from #LFTCM 2024 > Coq/Rocq tutorial and practice by Cyril Cohen.

[Cyril Cohen]

Cyril Cohen said:

Vincent Beffara said:

I'm just copy pasting commands I'm finding online ...

I know, just give me a few more minutes and I will give you a single command to type :sweat_smile:

If you pull the repo you should be able to type:

opam install -y --deps-only .

[Vincent Beffara]

It works! :tada:

[Vincent Beffara]

Still getting warnings like

Notation "_ + _" was already used in scope nat_scope
New coercion path [GRing.subring_closedM; GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing [GRing.subring_closedB;

but I'm assuming that is not an issue.

[Vincent Beffara]

Thanks!

[Cyril Cohen]

Vincent Beffara said:

Still getting warnings like

Notation "_ + _" was already used in scope nat_scope
New coercion path [GRing.subring_closedM; GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing [GRing.subring_closedB;

but I'm assuming that is not an issue.

Not an issue, indeed.

[Notification Bot]

5 messages were moved from this topic to #LFTCM 2024 > Coq/Rocq tutorial and practice, general troubleshooting by Cyril Cohen.

[Florent Schaffhauser]

Vincent Beffara said:

It works! :tada:

It works indeed! Thanks a lot @Cyril Cohen and @Marie Kerjean !

[Florent Schaffhauser]

Do you recommend Coq-LSP over VS-Coq as a VS code extension?

[Frédéric Dupuis]

The URL: https://github.com/CohenCyril/LFTCM2024_Rocq

[Cyril Cohen]

Flo (Florent Schaffhauser) said:

Do you recommend Coq-LSP over VS-Coq as a VS code extension?

I have no strong recommendation yet, both tools are too young to decide.