Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Can't build the project using a local opam switch #62

Open
Lesenr1 opened this issue Feb 25, 2024 · 3 comments
Open

Can't build the project using a local opam switch #62

Lesenr1 opened this issue Feb 25, 2024 · 3 comments

Comments

@Lesenr1
Copy link

Lesenr1 commented Feb 25, 2024 •
edited
Loading

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
Copy link
Contributor

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
Copy link
Author

Lesenr1 commented Feb 25, 2024

exact same result

@Lesenr1
Copy link
Author

Lesenr1 commented Feb 27, 2024

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

🥳

@Lesenr1 Lesenr1 changed the title Can't build the project Can't build the project using a local opam switch Feb 27, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@samuelgruetter @Lesenr1