Stream: Coq users

Topic: Project File Problem

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Brandon Sisler (Jan 08 2023 at 02:18):

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

view this post on Zulip Notification Bot (Jan 08 2023 at 08:39):

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

Last updated: Jun 17 2024 at 22:01 UTC