Can't build the project using a local opam switch

[Lesenr1]

Disclaimer: I am a coq noob
Edit: resolved by using a global opam switch

As stated in the .tex sources I used coq 8.16.0 (I also tried with 8.15.0 to 8.19.0).
I installed coq through opam

coq:

> opam exec -- coqtop -v
The Coq Proof Assistant, version 8.16.0
compiled with OCaml 4.13.1

operating system:

> lsb_release -a
No LSB modules are available.
Distributor ID: Ubuntu
Description:    Ubuntu 20.04 LTS
Release:        20.04
Codename:       focal

I get a Error: Cannot find a physical path bound to logical path Prelude with prefix Coq. error when running the makefile. There is also a handfull of warnings but I do not know if that is normal so here is the full output after opam exec -- make

make -f Makefile.coq Frap.vo AbstractInterpret.vo SepCancel.vo
make[1]: Entering directory '/home/lesenr1/work/frap'
COQC Sets.v
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/Compat was previously
bound to Coq.Compat; it is remapped to Frap._opam.lib.coq.theories.Compat
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/derive was previously
bound to Coq.derive; it is remapped to Frap._opam.lib.coq.theories.derive
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/Logic was previously
bound to Coq.Logic; it is remapped to Frap._opam.lib.coq.theories.Logic
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/QArith was previously
bound to Coq.QArith; it is remapped to Frap._opam.lib.coq.theories.QArith
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/Relations was
previously bound to Coq.Relations; it is remapped to
Frap._opam.lib.coq.theories.Relations [overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/rtauto was previously
bound to Coq.rtauto; it is remapped to Frap._opam.lib.coq.theories.rtauto
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/NArith was previously
bound to Coq.NArith; it is remapped to Frap._opam.lib.coq.theories.NArith
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/nsatz was previously
bound to Coq.nsatz; it is remapped to Frap._opam.lib.coq.theories.nsatz
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/FSets was previously
bound to Coq.FSets; it is remapped to Frap._opam.lib.coq.theories.FSets
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/Sorting was
previously bound to Coq.Sorting; it is remapped to
Frap._opam.lib.coq.theories.Sorting [overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/Array was previously
bound to Coq.Array; it is remapped to Frap._opam.lib.coq.theories.Array
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/Structures was
previously bound to Coq.Structures; it is remapped to
Frap._opam.lib.coq.theories.Structures [overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/funind was previously
bound to Coq.funind; it is remapped to Frap._opam.lib.coq.theories.funind
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/micromega was
previously bound to Coq.micromega; it is remapped to
Frap._opam.lib.coq.theories.micromega [overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/Vectors was
previously bound to Coq.Vectors; it is remapped to
Frap._opam.lib.coq.theories.Vectors [overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/Setoids was
previously bound to Coq.Setoids; it is remapped to
Frap._opam.lib.coq.theories.Setoids [overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/extraction was
previously bound to Coq.extraction; it is remapped to
Frap._opam.lib.coq.theories.extraction [overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/Init was previously
bound to Coq.Init; it is remapped to Frap._opam.lib.coq.theories.Init
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/Sets was previously
bound to Coq.Sets; it is remapped to Frap._opam.lib.coq.theories.Sets
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/setoid_ring was
previously bound to Coq.setoid_ring; it is remapped to
Frap._opam.lib.coq.theories.setoid_ring
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/ssr was previously
bound to Coq.ssr; it is remapped to Frap._opam.lib.coq.theories.ssr
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/PArith was previously
bound to Coq.PArith; it is remapped to Frap._opam.lib.coq.theories.PArith
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/omega was previously
bound to Coq.omega; it is remapped to Frap._opam.lib.coq.theories.omega
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/btauto was previously
bound to Coq.btauto; it is remapped to Frap._opam.lib.coq.theories.btauto
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/Reals/Abstract was
previously bound to Coq.Reals.Abstract; it is remapped to
Frap._opam.lib.coq.theories.Reals.Abstract
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/Reals/Cauchy was
previously bound to Coq.Reals.Cauchy; it is remapped to
Frap._opam.lib.coq.theories.Reals.Cauchy
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/Reals was previously
bound to Coq.Reals; it is remapped to Frap._opam.lib.coq.theories.Reals
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/ZArith was previously
bound to Coq.ZArith; it is remapped to Frap._opam.lib.coq.theories.ZArith
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/Strings was
previously bound to Coq.Strings; it is remapped to
Frap._opam.lib.coq.theories.Strings [overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/Lists was previously
bound to Coq.Lists; it is remapped to Frap._opam.lib.coq.theories.Lists
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/Classes was
previously bound to Coq.Classes; it is remapped to
Frap._opam.lib.coq.theories.Classes [overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/Wellfounded was
previously bound to Coq.Wellfounded; it is remapped to
Frap._opam.lib.coq.theories.Wellfounded
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/Unicode was
previously bound to Coq.Unicode; it is remapped to
Frap._opam.lib.coq.theories.Unicode [overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/Floats was previously
bound to Coq.Floats; it is remapped to Frap._opam.lib.coq.theories.Floats
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/MSets was previously
bound to Coq.MSets; it is remapped to Frap._opam.lib.coq.theories.MSets
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/Arith was previously
bound to Coq.Arith; it is remapped to Frap._opam.lib.coq.theories.Arith
[overriding-logical-loadpath,loadpath]
Warning:
/home/lesenr1/work/frap/_opam/lib/coq/theories/Numbers/Cyclic/Abstract was
previously bound to Coq.Numbers.Cyclic.Abstract; it is remapped to
Frap._opam.lib.coq.theories.Numbers.Cyclic.Abstract
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/Numbers/Cyclic/Int31
was previously bound to Coq.Numbers.Cyclic.Int31; it is remapped to
Frap._opam.lib.coq.theories.Numbers.Cyclic.Int31
[overriding-logical-loadpath,loadpath]
Warning:
/home/lesenr1/work/frap/_opam/lib/coq/theories/Numbers/Cyclic/ZModulo was
previously bound to Coq.Numbers.Cyclic.ZModulo; it is remapped to
Frap._opam.lib.coq.theories.Numbers.Cyclic.ZModulo
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/Numbers/Cyclic/Int63
was previously bound to Coq.Numbers.Cyclic.Int63; it is remapped to
Frap._opam.lib.coq.theories.Numbers.Cyclic.Int63
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/Numbers/Cyclic was
previously bound to Coq.Numbers.Cyclic; it is remapped to
Frap._opam.lib.coq.theories.Numbers.Cyclic
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/Numbers/NatInt was
previously bound to Coq.Numbers.NatInt; it is remapped to
Frap._opam.lib.coq.theories.Numbers.NatInt
[overriding-logical-loadpath,loadpath]
Warning:
/home/lesenr1/work/frap/_opam/lib/coq/theories/Numbers/Integer/Binary was
previously bound to Coq.Numbers.Integer.Binary; it is remapped to
Frap._opam.lib.coq.theories.Numbers.Integer.Binary
[overriding-logical-loadpath,loadpath]
Warning:
/home/lesenr1/work/frap/_opam/lib/coq/theories/Numbers/Integer/Abstract was
previously bound to Coq.Numbers.Integer.Abstract; it is remapped to
Frap._opam.lib.coq.theories.Numbers.Integer.Abstract
[overriding-logical-loadpath,loadpath]
Warning:
/home/lesenr1/work/frap/_opam/lib/coq/theories/Numbers/Integer/NatPairs was
previously bound to Coq.Numbers.Integer.NatPairs; it is remapped to
Frap._opam.lib.coq.theories.Numbers.Integer.NatPairs
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/Numbers/Integer was
previously bound to Coq.Numbers.Integer; it is remapped to
Frap._opam.lib.coq.theories.Numbers.Integer
[overriding-logical-loadpath,loadpath]
Warning:
/home/lesenr1/work/frap/_opam/lib/coq/theories/Numbers/Natural/Binary was
previously bound to Coq.Numbers.Natural.Binary; it is remapped to
Frap._opam.lib.coq.theories.Numbers.Natural.Binary
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/Numbers/Natural/Peano
was previously bound to Coq.Numbers.Natural.Peano; it is remapped to
Frap._opam.lib.coq.theories.Numbers.Natural.Peano
[overriding-logical-loadpath,loadpath]
Warning:
/home/lesenr1/work/frap/_opam/lib/coq/theories/Numbers/Natural/Abstract was
previously bound to Coq.Numbers.Natural.Abstract; it is remapped to
Frap._opam.lib.coq.theories.Numbers.Natural.Abstract
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/Numbers/Natural was
previously bound to Coq.Numbers.Natural; it is remapped to
Frap._opam.lib.coq.theories.Numbers.Natural
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/Numbers was
previously bound to Coq.Numbers; it is remapped to
Frap._opam.lib.coq.theories.Numbers [overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/Program was
previously bound to Coq.Program; it is remapped to
Frap._opam.lib.coq.theories.Program [overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/Bool was previously
bound to Coq.Bool; it is remapped to Frap._opam.lib.coq.theories.Bool
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories/ssrmatching was
previously bound to Coq.ssrmatching; it is remapped to
Frap._opam.lib.coq.theories.ssrmatching
[overriding-logical-loadpath,loadpath]
Warning: /home/lesenr1/work/frap/_opam/lib/coq/theories was previously bound
to Coq; it is remapped to Frap._opam.lib.coq.theories
[overriding-logical-loadpath,loadpath]
Error: Cannot find a physical path bound to logical path
Prelude with prefix Coq.

make[1]: *** [Makefile.coq:793: Sets.vo] Error 1
make[1]: Leaving directory '/home/lesenr1/work/frap'
make: *** [Makefile:16: lib] Error 2

[samuelgruetter]

Using opam exec seems non-standard to me, does it work better if you do eval $(opam env) and then invoke the programs such as coq or make directly?

[Lesenr1]

exact same result

[Lesenr1]

Someone helped me on discord and it seems that - for some reasons - we can't build the project with a local opam switch.
Instead, one have to create a global switch :

opam switch create ocaml.4.13
eval $(opam env)
opam install coq.8.16.0
make

🥳