search

achlipala / frap

Formal Reasoning About Programs
Other
657 stars 82 forks source link

Error with make all #63

Open fedeb95 opened 3 months ago

fedeb95 commented 3 months ago

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?

samuelgruetter commented 3 months ago

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 :wink:

fedeb95 commented 3 months ago

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.