Stream: Coq users

Topic: Project File Problem

Brandon Sisler (Jan 07 2023 at 23:24):

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?

Ana de Almeida Borges (Jan 08 2023 at 00:40):

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.

Brandon Sisler (Jan 08 2023 at 02:18):

Aha! The .vo file was the issue, also, very good to know about -Q . LF . Thanks!

Notification Bot (Jan 08 2023 at 08:39):

This topic was moved here from #Miscellaneous > Project File Problem by Karl Palmskog.

Last updated: Oct 13 2024 at 01:02 UTC