Stream: Coq devs & plugin devs

Topic: geocoq failing in bench


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Pierre Roux (May 17 2023 at 09:43):

It's indeed not in MC's CI since it's not in Nix

view this post on Zulip Pierre Roux (May 17 2023 at 11:28):

Here is a fixing PR: https://github.com/GeoCoq/GeoCoq/pull/40


Last updated: Jul 23 2024 at 17:01 UTC