Build issue [reference not found error]

[Unlimitosu]

I tried to build this library, and the following error occured.

unlimit@ubuntu:~/Documents/constant-time/coqword-2.1$ make
dune  build
Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
3.8 and will be removed in an upcoming Dune version.
File "./src/word_ssrZ.v", line 87, characters 24-31:
Error: The reference EqMixin was not found in the current environment.

make: *** [Makefile:13: build] Error 1

I found EqMixin is in ssreflect library, and I already installed it.

unlimit@ubuntu:~/Documents/constant-time/coqword-2.1$ opam list
# Packages matching: installed
# Name                  # Installed # Synopsis
...
coq                     8.17.1      pinned to version 8.17.1
coq-core                8.17.1      The Coq Proof Assistant -- Core Binaries and
coq-elpi                1.18.0      Elpi extension language for Coq
coq-hierarchy-builder   1.5.0       High level commands to declare and evolve a 
coq-mathcomp-algebra    2.0.0       Mathematical Components Library on Algebra
coq-mathcomp-fingroup   2.0.0       Mathematical Components Library on finite gr
coq-mathcomp-ssreflect  2.0.0       Small Scale Reflection
...

Here, I could find coq mathcomp libraries installed. But EqMixin in ssreflect cannot be found.

How can I solve this error?

Here are some versions I used: OCaml 5.0.0 / 4.14 opam 2.1.0 Coq Proof Assistant 8.17.1 (compiled with OCaml 5.0.0)

Thanks.

[vbgl]

This library is not yet compatible with mathcomp 2.0, so this error is expected.

Hint: https://github.com/jasmin-lang/coqword/blob/v2.1/coq-mathcomp-word.opam#L13

To work around this, you may install an earlier version of the coq-mathcomp-* libraries.

[Unlimitosu]

@vbgl Ok now I installed mathcomp with version 1.15.0 + Coq version 8.16.0.

Does this library need only make to build? I ran make and got following logs:

unlimit@ubuntu:~/Documents/constant-time/coqword-2.1/_build/default$ make
dune  build
Entering directory '/home/unlimit/Documents/constant-time/coqword-2.1'
Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
3.8 and will be removed in an upcoming Dune version.

but I cannot find it in opam list

unlimit@ubuntu:~/Documents/constant-time/coqword-2.1$ opam list | grep coq
coq                     8.16.0      Formal proof management system
coq-mathcomp-algebra    1.15.0      Mathematical Components Library on Algebra
coq-mathcomp-fingroup   1.15.0      Mathematical Components Library on finite groups
coq-mathcomp-ssreflect  1.15.0      Small Scale Reflection
coqide                  8.16.0      IDE of the Coq formal proof management system

how can I check if it is built correctly?

[strub]

Hi. If you want this library to be installed via opam, the simplest it to use the coq repository. Do

opam repo add coq-released https://coq.inria.fr/opam/released

and then you can opam install coq-mathcomp-word

[Unlimitosu]

@strub It works. Thanks a lot :)