Bas Spitters (Aug 13 2020 at 19:18): Bas Spitters (Aug 13 2020 at 19:18):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:
https://github.com/coq-community/vscoq
What am I overlooking?
Paolo Giarrusso (Aug 13 2020 at 19:30):Is _CoqProject in the root of the folder you opened with VsCoq? (BTW, this probably belongs in the VsCoq stream)
Paolo Giarrusso (Aug 13 2020 at 19:30):(Not 100% sure that’d explain it)
Bas Spitters (Aug 13 2020 at 19:33):That's also what I was thinking, but:
cat _CoqProject
-Q . LF
Paolo Giarrusso (Aug 13 2020 at 20:16):ah! I'd try moving all files into theoriesand updating _CoqProject
Paolo Giarrusso (Aug 13 2020 at 20:18):I do remember-Q . is a bad idea, but I forget exactly why; it might be that VsCoq doesn't support it well.
Karl Palmskog (Aug 13 2020 at 20:20):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...
Notification Bot (Aug 14 2020 at 08:55):This topic was moved here from #Coq users > vscode coqproject by Théo Zimmermann
Bas Spitters (Aug 14 2020 at 09:15):I guess @Maxime Dénès knows whether -Q is supported by vscoq
Paolo Giarrusso (Aug 14 2020 at 10:35):BTW, did you build the project first? Unlike Proof General, VsCoq does not do that for you
Paolo Giarrusso (Aug 14 2020 at 10:42):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.
Gaëtan Gilbert (Aug 14 2020 at 10:44):If you check ps maybe you can see what -Q vscoq passes to the subprocess
Bas Spitters (Aug 14 2020 at 10:59):@Paolo Giarrusso Thanks. Yes, the vo, vok, vos files are there.
Bas Spitters (Aug 14 2020 at 11:00):@Gaëtan Gilbert ps gives me a lot of arguments for code, but nothing that looks like it came from -Q
Paolo Giarrusso (Aug 14 2020 at 11:02):I assume the question is about the arguments to the coqtop or coqidetop subprocess
Bas Spitters (Aug 14 2020 at 11:04):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=
Paolo Giarrusso (Aug 14 2020 at 11:29):that suggests coq isn’t running, but the error you showed came from Coq... did Coq crash altogether ?
Bas Spitters (Aug 14 2020 at 11:47):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.
Paolo Giarrusso (Aug 14 2020 at 13:40):@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)
Paolo Giarrusso (Aug 14 2020 at 13:41):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.
Paolo Giarrusso (Aug 14 2020 at 13:42):E.g. image.png
Paolo Giarrusso (Aug 14 2020 at 13:43):The "Coq Language Server" part contains lots of output, but that's the relevant part.
Paolo Giarrusso (Aug 14 2020 at 13:43):Anyway, let me recheck my -Q . theory; it's probably easier.
Bas Spitters (Aug 14 2020 at 13:49):@Paolo Giarrusso I see no output there.
Paolo Giarrusso (Aug 14 2020 at 13:51):hm, -Q . seems to work even in VsCoq, so nevermind that theory
Paolo Giarrusso (Aug 14 2020 at 13:51):@Bas Spitters no output in your "Coq Language Server" view while Coq is running? Hm, that's unexpected :-(
Paolo Giarrusso (Aug 14 2020 at 13:52):(double-checked: Ubuntu snaps run in containers, which might explain why ps doesn't show the coq process. No idea about the rest).
Gaëtan Gilbert (Aug 14 2020 at 13:56):Why do you say ps doesn't show the coq process? your grep has coqidetop
Paolo Giarrusso (Aug 14 2020 at 14:06):Mine yes, but Bas's doesn't
Paolo Giarrusso (Aug 14 2020 at 14:06): Gaëtan Gilbert (Aug 14 2020 at 14:07):right
Bas Spitters (Aug 14 2020 at 14:19):At installation, I was warned that vscode does not respect the boundaries usually respected by snap packages.
Bas Spitters (Aug 14 2020 at 14:22):@Paolo Giarrusso Found it:
Detected coqtop version 8.11.2
Coqtop version parsed into semver version 8.11.2
Paolo Giarrusso (Aug 14 2020 at 14:23):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
Bas Spitters (Aug 14 2020 at 14:24):This seems to be a problem:
Loading project with no root directory
Changed path to:
Paolo Giarrusso (Aug 14 2020 at 14:27):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 ...
Paolo Giarrusso (Aug 14 2020 at 14:27):and I just successfully loaded Induction.v
Paolo Giarrusso (Aug 14 2020 at 14:29):@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 ?
Paolo Giarrusso (Aug 14 2020 at 14:29):but I agree this doesn't sound great.
Bas Spitters (Aug 14 2020 at 14:30):https://gist.github.com/spitters/bdd192b9bcc852cf68577f2137a5f678
Paolo Giarrusso (Aug 14 2020 at 14:43):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?
Paolo Giarrusso (Aug 14 2020 at 14:43):I guess https://coq.zulipchat.com/#narrow/stream/237662-VsCoq-devs.20.26.20users/topic/vscode.20coqproject/near/206859655 implies yes
Gaëtan Gilbert (Aug 14 2020 at 14:49):btw it shouldn't impact require but I'm pretty sure -topfile doesn't understand those file:// protocol prefixes
Bas Spitters (Aug 14 2020 at 14:53):@Paolo Giarrusso Thanks! With open folder everything works!
I just did what I do with emacs, start from the command line
code IndPrinciples.v
Bas Spitters (Aug 14 2020 at 14:56):I'm embarrassed. It's actually documented:
https://github.com/coq-community/vscoq
"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."
Maxime Dénès (Aug 14 2020 at 15:52):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
Maxime Dénès (Aug 14 2020 at 15:52):and to a proper format for project description files
Paolo Giarrusso (Aug 14 2020 at 16:02):@Bas Spitters it's still a bug that this needs to be documented :-)
Paolo Giarrusso (Aug 14 2020 at 16:16):could vscoq warn about this scenario, somehow?
Bas Spitters (Aug 14 2020 at 17:03):@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.
Paolo Giarrusso (Aug 14 2020 at 17:07):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”.
Paolo Giarrusso (Aug 14 2020 at 17:09):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.
Paolo Giarrusso (Aug 14 2020 at 17:11):(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: Jun 04 2023 at 23:30 UTC