Hello, I got that error on Coq:"Cannot find a physical path bound to logical path matching suffix <> and prefix LF."
I follow all the instructions to make .vo file and create it, but the error still remain. This is on the file "Induction.v" on the line number 9 :"From LF Require Export Basics." of software fundation" for learning Coq. Please do you have an idea to fix this ?
What editor/IDE are you using? And what Operating system? (Most likely the folder where Induction.v is located as well)
Did you run
make in the folder where the makefile is?
Thank for replying. I use MacOs and the editor is Vscode. And I ran make Basics.vo in directory of makefile .
you can probably just run
make basics.vo indicate that everything went well?
and you are opening the file
Induction.v in the same folder where Basics.vo and _CoqProject are, do you?
Yes ! And all thoses file are in the same folder.
does "Print LoadPath.", inserted and executed into the coq-file at the beginning, list something about
LF.? It probably lists a lot of things about
and is vscoq opened in the folder as well? You can just run
code . from the terminal to open vscode in the right folder
coq only sees the .vo file if _CoqProject is at the workspace root of vscode, which you can do by
File -> open Folder...
This is what it shows:
Hm, as I expected it does not see that the library
LF is in that folder
Well, if opening vscode with that folder as workspace does not work, there is a "hacky" solution:
Add LoadPath "/path/to/lf" as LF.
Add this to the beginning of the coq file and at least it will work. (of course you need to adjust the path ;) )
I get now with "Add LoadPath" that error : "Cannot open /jovial/Documents/COQ-dossiers/lf [cannot-open-path,filesystem]coqtop"
Oh, that seems somewhat macOs-specific, maybe the app does not have enough access rights because of sandboxing. Sorry, I can't help here.
how did you install coq on macos?
with Homebrew: brew install coq
new version of macos? (I heard that some update released a few weeks ago)
No, I didn't update the mac.
hm, maybe as a workaround, can you start
coqide in the folder?
Maybe @Michael Soegtrop or @Théo Winterhalter know more about macos, but I don't.
coqide is not in the folder "lf".
yes, that is toally ok. I thought that maybe homebrew installs the other ide,
coqide as well, and that you could just start it from command line, but this was a wild guess.
You could try installing with opam, the ocaml-packet-manager, but I'm not sure that helps: https://coq.inria.fr/opam-using.html
and that probably takes 30 minutes to compile coq
I wouldn't expect sandboxing tho?
@Jovial Cheukam what is the exact
LoadPath line you gave?
I'd be surprised if the path /jovial/Documents/COQ-dossiers/lf were correct...
I expect you need to add
/Users at the beginning of the path, e.g.
@Fabian Kunze is
File -> open Folder... an actual thing? Not here..
What I have to do in VSCode is "File -> New Windows", then "File -> Open", and finally select the right folder (aka the one containing
_CoqProject as Fabian said)
Paolo Giarrusso said:
Fabian Kunze is
File -> open Folder...an actual thing? Not here..
Under my linux-system, I have the option
Open Folder in my file menu in vscoq
Yeah we don't have it on macOS, but you can just use open and select a folder and it works I think.
Thanks. I added
/Users to the path and it's working well now.
What about running
code . from the console?
It would be best to find a solution that doesn't require
Add LoadPath because this is really hackish.
Last updated: Sep 30 2023 at 06:01 UTC