Stream: VsCoq devs & users

Topic: vscode coqproject


view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Paolo Giarrusso (Aug 13 2020 at 19:30):

(Not 100% sure that’d explain it)

view this post on Zulip Bas Spitters (Aug 13 2020 at 19:33):

That's also what I was thinking, but:

cat _CoqProject
-Q . LF

view this post on Zulip Paolo Giarrusso (Aug 13 2020 at 20:16):

ah! I'd try moving all files into theoriesand updating _CoqProject

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Notification Bot (Aug 14 2020 at 08:55):

This topic was moved here from #Coq users > vscode coqproject by Théo Zimmermann

view this post on Zulip Bas Spitters (Aug 14 2020 at 09:15):

I guess @Maxime Dénès knows whether -Q is supported by vscoq

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Aug 14 2020 at 10:44):

If you check ps maybe you can see what -Q vscoq passes to the subprocess

view this post on Zulip Bas Spitters (Aug 14 2020 at 10:59):

@Paolo Giarrusso Thanks. Yes, the vo, vok, vos files are there.

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Aug 14 2020 at 11:02):

I assume the question is about the arguments to the coqtop or coqidetop subprocess

view this post on Zulip 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=

view this post on Zulip 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 ?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Aug 14 2020 at 13:40):

(those would be found by grep coq, but I get more results)

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Aug 14 2020 at 13:42):

E.g. image.png

view this post on Zulip Paolo Giarrusso (Aug 14 2020 at 13:43):

The "Coq Language Server" part contains lots of output, but that's the relevant part.

view this post on Zulip Paolo Giarrusso (Aug 14 2020 at 13:43):

Anyway, let me recheck my -Q . theory; it's probably easier.

view this post on Zulip Bas Spitters (Aug 14 2020 at 13:49):

@Paolo Giarrusso I see no output there.

view this post on Zulip Paolo Giarrusso (Aug 14 2020 at 13:51):

hm, -Q . seems to work even in VsCoq, so nevermind that theory

view this post on Zulip 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 :-(

view this post on Zulip 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).

view this post on Zulip Gaëtan Gilbert (Aug 14 2020 at 13:56):

Why do you say ps doesn't show the coq process? your grep has coqidetop

view this post on Zulip Paolo Giarrusso (Aug 14 2020 at 14:06):

Mine yes, but Bas's doesn't

view this post on Zulip Paolo Giarrusso (Aug 14 2020 at 14:06):

see https://coq.zulipchat.com/#narrow/stream/237662-VsCoq-devs.20.26.20users/topic/vscode.20coqproject/near/206918223

view this post on Zulip Gaëtan Gilbert (Aug 14 2020 at 14:07):

right

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Aug 14 2020 at 14:23):

for me that's right after

view this post on Zulip Bas Spitters (Aug 14 2020 at 14:24):

This seems to be a problem:

Loading project with no root directory
Changed path to:

view this post on Zulip 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)
--------------------------------

view this post on Zulip Bas Spitters (Aug 14 2020 at 14:27):

The -Q is indeed absent. I only get:
-async-proofs on -topfile ...

view this post on Zulip Paolo Giarrusso (Aug 14 2020 at 14:27):

and I just successfully loaded Induction.v

view this post on Zulip 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 ?

view this post on Zulip Paolo Giarrusso (Aug 14 2020 at 14:29):

but I agree this doesn't sound great.

view this post on Zulip Bas Spitters (Aug 14 2020 at 14:30):

https://gist.github.com/spitters/bdd192b9bcc852cf68577f2137a5f678

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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."

view this post on Zulip 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

view this post on Zulip Maxime Dénès (Aug 14 2020 at 15:52):

and to a proper format for project description files

view this post on Zulip Paolo Giarrusso (Aug 14 2020 at 16:02):

@Bas Spitters it's still a bug that this needs to be documented :-)

view this post on Zulip Paolo Giarrusso (Aug 14 2020 at 16:16):

could vscoq warn about this scenario, somehow?

view this post on Zulip 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.

view this post on Zulip 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”.

view this post on Zulip 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.

view this post on Zulip 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: Jan 30 2023 at 17:03 UTC