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 [image] I ran coq_makefile -f _CoqProject *.v -o Makefile and make but I get an error Cannot find a physical path bound to logical pa…

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 fil…

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…

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

[image] chokristine: 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. S…

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. [image] But when I try to interpret lines of Induction.v I get Cannot find a phys…

Thank you! Turns out I had to configure the coqtop.coqProjectRoot in the extension setting [image] and make sure the coqtop bin path was set correctly [image] [image]

How to import Basics.v in Induction.v of LF using VS Coq extension

Using Rocq

brando90 February 24, 2023, 11:49pm 8

Topic		Replies	Views
Issue with importing definitions from previous chapter in CoqIDE Using Rocq software-foundations	24	598	July 10, 2024
How to have vscode find coq? Using Rocq	5	4943	February 24, 2023
Software Foundations: minustwo not found in Poly.v Using Rocq software-foundations	6	772	July 28, 2021
Coqtop is not running Using Rocq	8	1013	September 8, 2023
How to import a file in Coq? Using Rocq	6	4648	June 8, 2020

How to import Basics.v in Induction.v of LF using VS Coq extension

Related topics