I have the following folder structure:
- BaseDefs.v
- UsingBaseDefs.v
Here, BaseDefs.v contains definitions that I want to use in UsingBaseDefs.v. I tried to use the coqc BaseDefs.v command from the terminal and then I tried to import the module inside of UsingBaseDefs.v using:
Require Import BaseDefs.
This gives me the error
Cannot find a physical path bound to logical path BaseDefs
I am working inside of CoqIDE and from another thread (How do I import modules in Coq?) it seems as if this should work. How do I resolve this error and make the Import available ?
Edit: If I print the LoadPath using the Print LoadPath command inside of UsingBaseDefs.v I can see that BaseDefs is not listed here.
In short: you are probably missing a _CoqProject file.
The Coq build system use this _CoqProject file (see the reference manual) to know what files are part of a multi-file project when building. Accordingly, IDEs use this system as well to do the mapping between the logical path (the one used in the Require Import command) and the system directory structure. Without such a file, CoqIDE does not know what BaseDefs refers to.
In your case, the _CoqProject probably needs to be something like
-R . MyProject
BaseDefs.v
UsingBaseDefs.v
to be located in the same folder as your two files. The first line tells Coq to map the . folder to the logical name MyProject. The next two lines makes it aware of the two files you have in that project. You can find a more complete typical template for a Coq project here, with e.g. a MakeFile.