Error with make all
Opened this issue · 2 comments
Hi, I'm trying to build the project as stated in the README, but make all fails with
make -f Makefile.coq
make[1]: Entering directory '/home/bedef/Projects/coq/frap'
/bin/sh: line 1: /snap/coq-prover/34/coq-platform/bin//coqc: No such file or directory
COQDEP VFILES
/bin/sh: line 1: /snap/coq-prover/34/coq-platform/bin//coqdep: No such file or directory
/bin/sh: line 1: /snap/coq-prover/34/coq-platform/bin//coqc: No such file or directory
COQDEP VFILES
/bin/sh: line 1: /snap/coq-prover/34/coq-platform/bin//coqdep: No such file or directory
W: This Makefile was generated by Coq 8.18.0
W: while the current Coq version is
/bin/sh: line 1: /snap/coq-prover/34/coq-platform/bin//coqc: No such file or directory
COQDEP VFILES
/bin/sh: line 1: /snap/coq-prover/34/coq-platform/bin//coqdep: No such file or directory
make[2]: *** No rule to make target '.Makefile.coq.d', needed by 'Map.vo'. Stop.
make[1]: *** [Makefile.coq:409: all] Error 2
make[1]: Leaving directory '/home/bedef/Projects/coq/frap'
make: *** [Makefile:13: coq] Error 2
I'm a beginner with coq and have installed it with the snap package as stated here https://coq.inria.fr/download. What am I missing?
Unfortunately I don't understand why you're getting this error, and I can't reproduce it on my Ubuntu 24 (sudo snap install coq-prover works fine for me).
However, I would not recommend using snap, because (at the time of writing), snap gives you Coq 8.18.0, but frap has not yet been updated to 8.18.0. Guessing from to the few latest frap commits, I believe Coq 8.15 or 8.16 might work best. If you're on a linux distro and lucky, your distro might have one of these versions packaged, or else I'd bite the bullet and learn a few opam commands. A while ago I wrote up some notes here, which might still work today (but you'd have to replace the coq and ocaml version number by suitable values). Good luck 😉
thanks for the answer!
In the meantime I've also tried running make form inside CoqIDE, with one file of frap open. It compiled something, but stopped at some unification. This could be because of the version of coq used, will try later with those you recommended.