Pedro Abreu (Feb 28 2023 at 21:21): Pedro Abreu (Feb 28 2023 at 21:21):For some reason my vscode cannot find other compiled files of the same project, I'm guessing that maybe it is not loading the proper _CoqProject. Is there a way to have vscode print what _CoqProject was loaded by VSCoq?
I'm thinking of something along the lines of the Messages buffer on emacs, in which you'd have a line like this:
Coq project file detected: /Users/pedroabreu/gitprojects/tutoring/dale/CSE-505/hw5/_CoqProject.
Pedro Abreu (Feb 28 2023 at 21:23):Suggestions on what else should I look at to try to solve this issue is also welcome
Paolo Giarrusso (Feb 28 2023 at 21:26):The "Coq Language Server" pane should also have such output, but unless you change settings VsCoq will only check the project root
Paolo Giarrusso (Feb 28 2023 at 21:27):Where "project root" = the folder that you opened with VsCode
Pedro Abreu (Feb 28 2023 at 21:46):Sorry for the beginner question, I'm new to vscode. But how do I open this pane?
Laurent Théry (Feb 28 2023 at 21:52):in View . click on Output [Ctrl + K Ctrl + H], then in the PullDown of the output view select Coq Language Server
Pedro Abreu (Feb 28 2023 at 21:53):oh got it!! thank you!
Pedro Abreu (Feb 28 2023 at 22:05):awesome, I could find the issue. I was opening the project on the parent file (I didn't know this matters in vscode), so it wasn't loading the proper _CoqProject file. Thanks for the help guys!
Notification Bot (Feb 28 2023 at 22:05):Pedro Abreu has marked this topic as resolved.
Last updated: Jun 04 2023 at 22:30 UTC