Théo Winterhalter (May 09 2024 at 02:18): Théo Winterhalter (May 09 2024 at 02:18):I installed Trocq using the instructions, but just
From Trocq Require Import Common.
produces
Error: Notation "~ _" is already defined at level 75 with arguments constr
at level 75 while it is now required to be at level 35 with arguments
constr at level 35.
Do I need to use Coq with -noinit?
Théo Winterhalter (May 09 2024 at 02:24):I'm guessing now that for now Trocq can't be used with mathcomp.
Théo Winterhalter (May 09 2024 at 07:51):We also wanted to use Trocq with Coq 8.19 and with @Reynald Affeldt we were able to fix a proof that broke because of a change in Coq-HoTT but then Coq-ELPI custom works only for 8.17. Just to let you know. :smile:
Théo Winterhalter (May 09 2024 at 08:03):I also tried to apply the changes of Enzo naively to Coq-ELPI master but I get errors in the tests (very verbose). And make install fails too.
Cyril Cohen (May 11 2024 at 17:48):Théo Winterhalter said:
I also tried to apply the changes of Enzo naively to Coq-ELPI master but I get errors in the tests (very verbose). And
make installfails too.
see https://github.com/LPCIC/coq-elpi/pull/585
Cyril Cohen (May 11 2024 at 17:49):Théo Winterhalter said:
I'm guessing now that for now Trocq can't be used with mathcomp.
Yes I know, I'm working on this https://github.com/coq-community/trocq/pull/9 when I'm not on vac
Théo Winterhalter (May 12 2024 at 00:16):Ah ok, I looked at the branches but couldn't guess. We figured you were working on it, just wanted to make sure it was currently not possible. Thanks.
Last updated: Oct 13 2024 at 01:02 UTC