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.

Answer 1

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.