Coq module "Cannot find a physical path bound to logical path matching suffix <> and prefix" and "not found in the loadpath"

Question

I'm reading logical foundations and have downloaded the coq scripts which come with it.

I'm using coq v8.8.1, install via opam.

I'm getting the two errors in the title, and I am not sure how I should go about debugging them.

The full error message for the second error is

COQDEP VFILES

*** Warning: in file Auto.v, library LF.Maps is required and has not been found in the loadpath!

My objective is to compile and run the Induction.v file. I used coqide's options to first "make makefile" and then "make" before I got these errors.

Software foundations comes with its own makefile. Try unpacking the tarball and running make in the top-level directory, without using coqide's makefile. — Arthur Azevedo De Amorim, Apr 04 '19 at 13:02
You can also check whether *.vo files were generated. These are compiled *.v files, so their presence indicates whether the source files were compiled successfully. — eponier, Apr 05 '19 at 13:28

score 2 · Answer 1 · answered Jan 25 '21 at 00:02

This worked for me:

Run this in the same directory as Basics.v

coqc -Q . LF Basics.v

And then...

I was able to compile Induction.v:
```
coqc -Q . LF Induction.v
```

And I was able to do this:

coqtop -Q . LF
{* now that coqtop is open... *}
From LF Require Export Basics.

Coq module "Cannot find a physical path bound to logical path matching suffix <> and prefix" and "not found in the loadpath"

1 Answers1