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.
```

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.

I'm trying to build the main branch of mczify, with version 8.11.2 and mathcomp 1.11 (ssreflect is 1.11)

ie the one there https://github.com/math-comp/mczify

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)

ok

I'm upgrading coq

doesn't work any better with coq 8.12 :/

or is there a dependency I miss ?

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.

Ok, will give a try

@Christian Doczkal you were right, coq-8.12 works

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: Jul 15 2024 at 19:01 UTC