search

coq-quantum / CoqQ

MIT License
16 stars 1 forks source link

Cannot find a physical path bound to logical path all_ssreflect with prefix mathcomp. #3

Closed jricc closed 11 months ago

jricc commented 11 months ago

Hello, I installed CoqQ and these dependencies with 

opam switch create \
    --yes \
    --deps-only \
    --packages=coq-mathcomp-analysis=0.5.2,coq-mathcomp-fingroup=1.14.0 \
    --repositories=default=https://opam.ocaml.org,coq-released=https://coq.inria.fr/opam/released \
    .

And 

opam
config exec -- make

The result is:

# Packages matching: installed
# Name                   # Installed # Synopsis
...
coq                      8.15.2      Formal proof management system
coq-elpi                 1.13.0      Elpi extension language for Coq
coq-hierarchy-builder    1.2.1       High level commands to declare and evolve a hierarchy based on packed classes
coq-mathcomp-algebra     1.14.0      Mathematical Components Library on Algebra
coq-mathcomp-analysis    0.5.2       An analysis library for mathematical components
coq-mathcomp-bigenough   1.0.1       A small library to do epsilon - N reasoning
coq-mathcomp-field       1.14.0      Mathematical Components Library on Fields
coq-mathcomp-fingroup    1.14.0      Mathematical Components Library on finite groups
coq-mathcomp-finmap      1.5.2       Finite sets, finite maps, finitely supported functions
coq-mathcomp-real-closed 1.1.4       Mathematical Components Library on real closed fields
coq-mathcomp-solvable    1.14.0      Mathematical Components Library on finite
...
dune                     3.12.1      Fast, portable, and opinionated build system
elpi                     1.14.3      ELPI - Embeddable λProlog Interpreter
...
ocaml                    4.13.1      The OCaml compiler (virtual package)
...

But when I try to use it, I have this error : Cannot find a physical path bound to logical path all_ssreflect with prefix mathcomp. Could you help me ?

strub commented 11 months ago

Hi. Do you have coq-mathcomp-ssreflect installed?

jricc commented 11 months ago

Thank you for your reply. I did have coq-mathcomp-ssreflect installed, but after a fresh reinstall from the beginning, everything is now working correctly.