Gaëtan Gilbert (May 17 2023 at 09:03): Gaëtan Gilbert (May 17 2023 at 09:03):eg https://gitlab.com/coq/coq/-/jobs/4292681091 which says
- File "./Meta_theory/Models/POF_to_Tarski.v", line 157, characters 0-69:
- Error: pattern v2 does not match LHS of dotC
-
- make[1]: *** [Makefile:810: Meta_theory/Models/POF_to_Tarski.vo] Error 1
we do have geocoq in CI, the same pipeline had https://gitlab.com/coq/coq/-/jobs/4292681194 which succeeded
Maybe it's incompatible with the mathcomp in the bench?
Enrico Tassi (May 17 2023 at 09:06):likely, the fix upstream could be as simple as calling "simpl", but I guess it is not in MC's CI, since I don't see an hb branch. CC @Pierre Roux
Pierre Roux (May 17 2023 at 09:43):It's indeed not in MC's CI since it's not in Nix
Pierre Roux (May 17 2023 at 11:28):Here is a fixing PR: https://github.com/GeoCoq/GeoCoq/pull/40
Last updated: Nov 29 2023 at 21:01 UTC