https://coq.vercel.app/ext/sf/lf/full/Induction.html
I am using VSCode Coq extension.
I am having an error with
From LF Require Export Basics.
in Induction.v
I ran coq_makefile -f _CoqProject *.v -o Makefile
and make but I get an error
Cannot find a physical path bound to logical path
Basics with prefix LF.
How do I load Basics.v
Has anyone successfully ran Induction.v file in the LF repository in VSCode? using the VSCoq extension?
Hi! What I did when I had this problem is made sure I downloaded the entire LF repository (So one giant folder that has everything in it) which you can just download from the Foundations Textbook Github. That already has the make file and everything like that inside of it. So after downloading it, I just opened up Basics in Coq, when to the “Compile” header next to tools at the very top, did compile buffer. It should make the files that you need to import it from then on.
I think the problem is with the "coqtop.coqProjectRoot" setting - according to the documentation, it is relative to the workspace root, which I think is the dev-notes directory (the top-level you have open in VSCode), so try setting it to "coq" (the directory that contains the .v and _CoqProject files).
Your _CoqProject needs to list Basics.v and maybe other files. Probably the *.v didn’t match Basics.v because it looked in the wrong directory.
You also need to run make after running coq_makefile so there is a Basics.vo file in the directory containing Basics.v…
Disclaimer: I don’t use vsCode
Are you using VSCoq extension in VSCode?
I tried to run Induction.v from the entire LF repo with VSCoq, but ran into the same error Cannot find a physical path bound to logical path Basics with prefix lf.
Appreciate the suggestion.
In VSCode, after running
coq_makefile -f _CoqProject *.v -o Makefile
make
produces Basics.vo and will print out any references to Basics.v in Induction.v.
Note the bottom right output.
But when I try to interpret lines of Induction.v I get Cannot find a physical path bound to logical path Basics with prefix lf.
Thank you! Turns out I had to configure the coqtop.coqProjectRoot in the extension setting
and make sure the coqtop bin path was set correctly
