Installation not working

[henriquebg99]

Hi!

I installed Coq-Sniper on a new switch, following the instructions on README.md: opam switch create 4.07.1 opam repo add coq-released https://coq.inria.fr/opam/released opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev opam install coq-sniper

I reloaded the shell, to update the env, and checked the versions.

The Coq Proof Assistant, version 8.15.2
compiled with OCaml 4.07.1

When I run coqc testsniper.v, I get the following:

File "./testsniper.v", line 1, characters 0-22:
Error: Cannot find a physical path bound to logical path Sniper.

./testsniper.v has the following:

Require Import Sniper.

Do you have any clues to solve this?

[louiseddp]

Hello,

Thank you for taking interest in Sniper ! Yes, some information in the README's main branch is certainly out of date (and the opam release too) as we are currently working on porting the plugin on recent Coq versions (and we are working on a Sniper version 2.0). I would recommend cloning this branch https://github.com/smtcoq/sniper/tree/coq-8.17-with-trakt, then running:

opam switch create 4.09.1
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
opam install . 

So use a more recent version of OCaml's compiler and also the local coq-sniper.opam file rather than the release ! Let me know if it works :)

[henriquebg99]

Hello, Louise, thank you a lot for your message!

I followed exactly the 4 commands you gave, but the result is the same. When I run coqc, I have always the same message:

File "./examples/example_picube.v", line 2, characters 0-22:
Error: Cannot find a physical path bound to logical path Sniper.

I checked the version:

$ opam list
...
coq-smtcoq              dev         pinned to version dev at git+https://github.com/smtcoq/smtcoq.git#with-trakt-coq-8.17
coq-sniper              dev+8.16    pinned to version dev+8.16 at git+file:///home/henrique/Documents/phd/rob/sniper#coq-8.17-with-trakt
coq-stdlib              8.17.1      The Coq Proof Assistant -- Standard Library
coq-trakt               1.2         pinned to version 1.2 at git+https://github.com/ecranceMERCE/trakt.git#1.2
coqide                  8.17.1      The Coq Proof Assistant --- GTK3 IDE
...
ocaml                   4.09.1      The OCaml compiler (virtual package)
ocaml-base-compiler     4.09.1      Official release 4.09.1
ocaml-compiler-libs     v0.12.4     OCaml compiler libraries repackaged
ocaml-config            1           OCaml Switch Configuration

Everything seems installed.

However, I checked the directory ~/.opam/4.09.1/lib/, and even though I found a lot of packages, such as smtcoq, I could not find sniper.

~/.opam/4.09.1/lib$ l -l
total 268
...
drwxrwxr-x  2 henrique henrique  4096 dez 21 09:40 coq-smtcoq/
...

The command ~/.opam/4.09.1/lib$ ls -l | grep "sniper" gives no output!

Any clues?

Thank you again for your time!

[louiseddp]

And if you try make or make test at the root instead of coqc ? I am not sure that using coqc is a good solution as Sniper has a Makefile

And for the examples, I compile them with make test but to see what is happening I always interpret them in my IDE, for some reason the IDE is able to find Sniper while coqc is not. The file example_picube.v was made for a seminar, I suggest that you interpret it in your IDE rather than using coqc on it, but the other examples are compiled with make test.

Also, as I suggested that you install Sniper using the coq-sniper.opam rather than using the package, you can add Add Rec LoadPath ".." as Sniper. in the example_picube.v file before importing Sniper.

[henriquebg99]

I tried make and then make install, and it works in CoqIDE. In coqc it does not work, but CoqIDE is enough for me! Merci, Louise, greetings from Lisbon.

[ckeller]

Hi @henriquebg99 To complete @louiseddp answers: to be able to use coqc, you simply have to replace Require Import Sniper. in the header of the file with From Sniper Require Import Sniper.. Best