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…

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

Using Coq

onlychans1 April 14, 2022, 2:29am 7

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

1 Like

How to have vscode find coq?

Topic		Replies	Views
How to import a file in Coq? Using Coq	6	3566	June 8, 2020
How to use "Require Import" Using Coq	1	1976	December 6, 2019
Building a project with coq_makefile, using a library specified in .coqrc Using Coq	0	529	January 25, 2022
How does one import native cyclic integers in coq? Using Coq	3	219	August 2, 2023
Add LoadPath in Coq 8.12.2 Using Coq	5	2017	March 22, 2021

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

Related Topics