Stream: math-comp users

Topic: Installation of mathcomp2 with 'make'


view this post on Zulip Congyan (Cruise) Song (Nov 07 2023 at 20:24):

Hi, we are having trouble with installation of mathcomp2 using 'make', following the guide from here.

/cygdrive/c/Coq-Platform~8.16~2022.09/bin/coq_makefile  -f Make -o Makefile.coq
/usr/bin/make -f Makefile.coq --no-print-directory
COQC ssreflect/binomial.v
File ".\ssreflect/binomial.v", line 71, characters 11-50:
Error:
HB.pack: not a type: In environment
p : nat
dFact : forall n : nat, 0 < n -> (n.-1)`! = \prod_(0 <= i < n | i != 0) i
lt1p : 1 < p
p_gt0 : 0 < p
pr_p : prime p
Fp1 := Ordinal lt1p : 'I_p
Fp0 := Ordinal p_gt0 : 'I_p
ltp1p : p.-1 < p
Fpn1 := Ordinal ltp1p : 'I_p
eqF1n1 : (Fp1 == Fpn1) = false
toFpP : forall m : nat, m %% p < p
toFp := fun n : nat => Ordinal (toFpP n) : nat -> 'I_p
mFp := fun i j : 'I_p => toFp (i * j) : 'I_p -> 'I_p -> 'I_p
Fp_mod : forall i : 'I_p, i %% p = i
mFpA : associative mFp
mFpC : commutative mFp
mFp1 : left_id Fp1 mFp
mFp1r : right_id Fp1 mFp
mFpcM := Monoid.isComLaw.phant_Build mFpA mFpC mFp1
 : Monoid.isComLaw.axioms_ 'I_p Fp1 mFp
The term "mFp" has type "'I_p -> 'I_p -> 'I_p"
which should be Set, Prop or Type.

make[2]: *** [Makefile.coq:793: ssreflect/binomial.vo] Error 1
make[1]: *** [Makefile.coq:409: all] Error 2
make: *** [Makefile.common:99: this-build] Error 2

The above error occurs when it tried to compile the binomial.v file, and we are wondering whether this is an error specific to us.

view this post on Zulip Paolo Giarrusso (Nov 07 2023 at 20:27):

which packages do you have installed? that Coq platform for 8.16 includes Coq 8.16 (good) and some old mathcomp version (which might cause trouble)

view this post on Zulip Karl Palmskog (Nov 07 2023 at 20:28):

yes, this looks to me like you're building a MathComp 2 package with MathComp 1 package installed (they are incompatible)

view this post on Zulip Paolo Giarrusso (Nov 07 2023 at 20:28):

using opam would uninstall the old mathcomp and make such problems impossible :-)

view this post on Zulip Karl Palmskog (Nov 07 2023 at 20:36):

yes, we highly recommend installing MathComp via opam, there are packages for MathComp 2.0.0 and 2.1.0 in the released opam repo

view this post on Zulip Congyan (Cruise) Song (Nov 08 2023 at 05:59):

Paolo Giarrusso said:

which packages do you have installed? that Coq platform for 8.16 includes Coq 8.16 (good) and some old mathcomp version (which might cause trouble)

Thank you for your reply, I have the Coq 8.16.1 installed, and there are indeed some old mathcomp lib that came with it such as 'multinomials' and 'word'.

view this post on Zulip Congyan (Cruise) Song (Nov 08 2023 at 06:00):

Karl Palmskog said:

yes, we highly recommend installing MathComp via opam, there are packages for MathComp 2.0.0 and 2.1.0 in the released opam repo

Thank you for your advice! I will try to use opam to reinstall it.


Last updated: Jul 25 2024 at 16:02 UTC