I'm trying vscode on SF for the first time. I get:
Cannot find a physical path bound to logical path matching suffix <> and prefix LF.
_Coqproject is enabled in the vscode settings, and the file works with proof general.
Otherwise, the settings are as recommended here:
What am I overlooking?
Is _CoqProject in the root of the folder you opened with VsCoq? (BTW, this probably belongs in the VsCoq stream)
(Not 100% sure that’d explain it)
That's also what I was thinking, but:
-Q . LF
ah! I'd try moving all files into
theoriesand updating _CoqProject
I do remember
-Q . is a bad idea, but I forget exactly why; it might be that VsCoq doesn't support it well.
hmm, in the realm of
coq_makefile and Dune,
-Q . <name> works quite well. Sadly, many projects use this and put all their source files in the root directory...
This topic was moved here from #Coq users > vscode coqproject by Théo Zimmermann
I guess @Maxime Dénès knows whether -Q is supported by vscoq
BTW, did you build the project first? Unlike Proof General, VsCoq does not do that for you
And sorry I didn’t think of this first. Re -Q, I’m sure that works, it’s
-Q . I have questions on. But I can test that separately.
If you check ps maybe you can see what -Q vscoq passes to the subprocess
@Paolo Giarrusso Thanks. Yes, the vo, vok, vos files are there.
@Gaëtan Gilbert ps gives me a lot of arguments for code, but nothing that looks like it came from -Q
I assume the question is about the arguments to the
ps -aux |grep coq
/snap/code/40/usr/share/code/code /home/spitters/.vscode/extensions/maximedenes.vscoq-0.3.2/out/server/src/server.js --node-ipc --clientProcessId=
that suggests coq isn’t running, but the error you showed came from Coq... did Coq crash altogether ?
I did not paste the ProcessId.
Coq is running, as it's generating the error message.
Coq is also working fine on other files (Basics). It works on Induction, until it imports Basics somewhere halfway.
@Bas Spitters I agree coq must be running to get that error — but that's clearly not shown by the
ps output, so
ps isn't showing the right thing. For instance, while processing
hkdot.v, I get:
$ ps aux|grep hkdot.v pgiarrusso 75732 0.0 0.0 4837652 400 ?? S 8:44pm 0:00.19 /Users/pgiarrusso/.opam/iris-3.3-coq-8.11.2/bin/coqproofworker.opt -main-channel stdfds -Q _build/default/theories D -w -notation-overridden -w -redundant-canonical-projection -w -convert_concl_no_check -w -undeclared-scope -w -ambiguous-paths -topfile file:///Users/pgiarrusso/git/gDOT/dot-iris/theories/Dot/hkdot/hkdot.v -worker-id proofworker:54 -async-proofs-worker-priority high pgiarrusso 75182 0.0 0.0 5797988 508 ?? S 8:43pm 1:10.78 /Users/pgiarrusso/.opam/iris-3.3-coq-8.11.2/bin/coqidetop.opt -main-channel 127.0.0.1:57182:57181 -control-channel 127.0.0.1:57183:57184 -async-proofs on -Q _build/default/theories D -w -notation-overridden -w -redundant-canonical-projection -w -convert_concl_no_check -w -undeclared-scope -w -ambiguous-paths -topfile file:///Users/pgiarrusso/git/gDOT/dot-iris/theories/Dot/hkdot/hkdot.v
(those would be found by
grep coq, but I get more results)
maybe those processes are hidden by the implementation of snaps... instead of debugging that, the "Coq Language Server" view in VSCode could be more helpful.
The "Coq Language Server" part contains lots of output, but that's the relevant part.
Anyway, let me recheck my
-Q . theory; it's probably easier.
@Paolo Giarrusso I see no output there.
-Q . seems to work even in VsCoq, so nevermind that theory
@Bas Spitters no output in your "Coq Language Server" view while Coq is running? Hm, that's unexpected :-(
(double-checked: Ubuntu snaps run in containers, which might explain why
ps doesn't show the coq process. No idea about the rest).
Why do you say ps doesn't show the coq process? your grep has coqidetop
Mine yes, but Bas's doesn't
At installation, I was warned that vscode does not respect the boundaries usually respected by snap packages.
@Paolo Giarrusso Found it:
Detected coqtop version 8.11.2
Coqtop version parsed into semver version 8.11.2
okay, we're looking for the line starting coqidetop, e.g.:
exec: /Users/pgiarrusso/.opam/iris-3.3-coq-8.11.2/bin/coqidetop.opt -main-channel 127.0.0.1:51132:51131 -control-channel 127.0.0.1:51134:51133 -async-proofs on -Q _build/default/theories D -w -notation-overridden -w -redundant-canonical-projection -w -convert_concl_no_check -w -undeclared-scope -w -ambiguous-paths -topfile file:///Users/pgiarrusso/git/gDOT/dot-iris/theories/Dot/hkdot/hkdot.v coqtop started with pid 25922
for me that's right after
This seems to be a problem:
Loading project with no root directory
Changed path to:
That sounds indeed bad, and potentially connected to snaps, not enough clue — on DeepSpec's LF, my startup sequence (on Mac) is
Coq Language Server: process.version: v12.8.1, process.arch: x64} Loaded project at /Users/pgiarrusso/OneDrive/Downloads-old/lf Changed path to: /Users/pgiarrusso/.opam/iris-3.3-coq-8.11.2/bin starting coqtop exec: /Users/pgiarrusso/.opam/iris-3.3-coq-8.11.2/bin/coqtop -v Listening at 127.0.0.1:54693 Listening at 127.0.0.1:54694 Listening at 127.0.0.1:54695 Listening at 127.0.0.1:54696 Detected coqtop version 8.11.2 Coqtop version parsed into semver version 8.11.2 exec: /Users/pgiarrusso/.opam/iris-3.3-coq-8.11.2/bin/coqidetop.opt -main-channel 127.0.0.1:54694:54693 -control-channel 127.0.0.1:54696:54695 -async-proofs on -Q . LF -topfile file:///Users/pgiarrusso/OneDrive/Downloads-old/lf/Induction.v coqtop started with pid 31094 Client connected on main channel R (port 54694) Client connected on main channel W (port 54693) Client connected on control channel R (port 54696) Client connected on control channel W (port 54695) --------------------------------
The -Q is indeed absent. I only get:
-async-proofs on -topfile ...
and I just successfully loaded
@Bas Spitters could you please past the entirety of the "Coq Language Server" content into a gist? I guess you can click there, and then select and copy all with Ctrl-A, and Ctrl-C ?
but I agree this doesn't sound great.
And when you started VSCode, and used "File -> Open" to open a folder, you did open the
/home/spitters/teaching/SF/sfdev/lf folder, right?
I guess https://coq.zulipchat.com/#narrow/stream/237662-VsCoq-devs.20.26.20users/topic/vscode.20coqproject/near/206859655 implies yes
btw it shouldn't impact require but I'm pretty sure -topfile doesn't understand those file:// protocol prefixes
@Paolo Giarrusso Thanks! With open folder everything works!
I just did what I do with emacs, start from the command line
I'm embarrassed. It's actually documented:
"if you use _CoqProject - start vscode via code my/project/root (or code . from the root folder of your project), or else select File|Open Folder... from vscode's menu."
I hope to improve the support of projects in VsCoq soon, but we are also waiting for Coq to converge on a way to build user projects
and to a proper format for project description files
@Bas Spitters it's still a bug that this needs to be documented :-)
could vscoq warn about this scenario, somehow?
@Paolo Giarrusso I don't know enough about vscode. It could for example pick up the error message and react to that, or there could be a general warning when starting vscode.
Right, sorry, the second question was more for @Maxime Dénès , but I’m not sure how that’d work. My only idea is “search for _CoqProject starting from the folder containing the .v file, and moving outward”.
I’ll mention that on e.g. Nix installs (and in general) the implementation would need to scan folders efficiently and in O(1) space. Agda searches for “project files” this way, but the directory scanning code reads a whole folder at once, which takes ~1GB and 20seconds on /nix or /nix/store.
(In that case, good O(1) directory scanning APIs are even missing; no idea of the state of the JS ecosystem on this front, tho I’d hope it’s better).
Last updated: Jan 30 2023 at 17:03 UTC