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.

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)

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

using `opam`

would uninstall the old `mathcomp`

and make such problems impossible :-)

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

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

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