Stream: math-comp users

Topic: mczify


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

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

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

view this post on Zulip vlj (Sep 27 2020 at 12:09):

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

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

view this post on Zulip vlj (Sep 27 2020 at 12:59):

ok

view this post on Zulip vlj (Sep 27 2020 at 12:59):

I'm upgrading coq

view this post on Zulip vlj (Sep 27 2020 at 13:00):

doesn't work any better with coq 8.12 :/

view this post on Zulip vlj (Sep 27 2020 at 13:01):

or is there a dependency I miss ?

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

view this post on Zulip vlj (Sep 27 2020 at 14:21):

Ok, will give a try

view this post on Zulip vlj (Sep 27 2020 at 19:08):

@Christian Doczkal you were right, coq-8.12 works

view this post on Zulip 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: Jan 29 2023 at 18:03 UTC