Hey all, I have been working on problems from the book Software Foundations, and am having the issue that when I try and import other files from the project folder I get an error.
For example, the line
From LF Require Export ProofObjects. I recieve the error
Cannot find a physical path bound to logical path ProofObjects with prefix LF.
Where "LF" is the folder name and has the associated
_CoqProject folder containing
-Q . LF
Any suggestion on what could be wrong?
What does your file tree look like? The statement
-Q . LF instructs Coq that files in the directory where
_CoqProject lives shall be identified by the
LF prefix. Thus, the folder being named
LF is irrelevant in this context. (Also,
_CoqProject should be a file without any extensions, not a folder, but I suppose that was a typo). If
ProofObjects.vo is not in the same directory as
_CoqProject, that would explain the error. This could be because
ProofObjects.v hasn't been compiled yet, or because it is simply somewhere else.
Aha! The .vo file was the issue, also, very good to know about
-Q . LF . Thanks!
This topic was moved here from #Miscellaneous > Project File Problem by Karl Palmskog.
Last updated: Oct 04 2023 at 23:01 UTC