vlj (Sep 27 2020 at 10:51): vlj (Sep 27 2020 at 10:51):Hi, I'm trying to build mczify via "make" (I installed coq via opam) and I have a build error : File "./theories/zify.v", line 13, characters 5-23:
Error: There is no Ltac named Zify.zify_pre_hook.
Christian Doczkal (Sep 27 2020 at 11:51):I think you need to be more specific about the versions of coq and mathcomp that you have installed and the version of mczify that you are trying to install.
vlj (Sep 27 2020 at 12:09):I'm trying to build the main branch of mczify, with version 8.11.2 and mathcomp 1.11 (ssreflect is 1.11)
vlj (Sep 27 2020 at 12:09):ie the one there https://github.com/math-comp/mczify
Paolo Giarrusso (Sep 27 2020 at 12:47):They require “The master branch of Coq (after 8.11)”; maybe that means you need Coq 8.12, but I can’t tell (and somebody should submit a clarification to their README)
vlj (Sep 27 2020 at 12:59):ok
vlj (Sep 27 2020 at 12:59):I'm upgrading coq
vlj (Sep 27 2020 at 13:00):doesn't work any better with coq 8.12 :/
vlj (Sep 27 2020 at 13:01):or is there a dependency I miss ?
Christian Doczkal (Sep 27 2020 at 13:28):Presumably, the latest version (e.g., master) only works with coq.dev and mathcomp.dev. However, there are branches called coq-8.11 and coq-8.12. So I suggest trying the branch matching your version of Coq.
vlj (Sep 27 2020 at 14:21):Ok, will give a try
vlj (Sep 27 2020 at 19:08):@Christian Doczkal you were right, coq-8.12 works
Karl Palmskog (Sep 28 2020 at 08:30):the basic problem here in my mind is that mczify has not been tagged and packaged on opam for different versions of Coq. Now that the project is in the MathComp organization, are there any plans to do this? See: https://github.com/math-comp/mczify/issues/12
Both Michael and I have offered to help with this, since there is currently no reliable way to use lia with MathComp across several Coq versions - depending on an opam package that has several versions for different Coq would solve this.
Last updated: Apr 19 2024 at 10:02 UTC