vscoq passes incorrect -topfile argument

[Blaisorblade]

vscoq uses -topfile file:///path or -topfile untitled:/path, but Coq demands a path (relative or absolute, doesn't matter); that path is compared against the -Q/-R options to compute the correct name of the module being created.

For instance, assume _CoqProject consists of -Q theories D, and test_topfile.v is the following:

Definition hello := Prop.
About hello.
Check D.test_topfile.hello.

This code (based on the testcase in ProofGeneral/PG#407 (comment)) compiles fine and works in coqtop with the correct options, but VSCoq fails to step through it.

Example incorrect command lines that VSCoq uses:

exec: /Users/pgiarrusso1/.opam/__coq-platform.2021.11.0~8.14~2021.11/bin/coqidetop.opt -main-channel 127.0.0.1:58104:58105 -control-channel 127.0.0.1:58106:58107 -async-proofs on -Q theories D -w -notation-overridden -w -redundant-canonical-projection -w -convert_concl_no_check -w -undeclared-scope -w -ambiguous-paths -w -deprecated-hint-rewrite-without-locality -w -deprecated-instance-without-locality -w -deprecated-typeclasses-transparency-without-locality -topfile untitled:/Users/pgiarrusso1/git/gDOT/dot-iris-make/theories/test_topfile.v

exec: /Users/pgiarrusso1/.opam/__coq-platform.2021.11.0~8.14~2021.11/bin/coqidetop.opt -main-channel 127.0.0.1:58158:58155 -control-channel 127.0.0.1:58156:58157 -async-proofs on -Q theories D -w -notation-overridden -w -redundant-canonical-projection -w -convert_concl_no_check -w -undeclared-scope -w -ambiguous-paths -w -deprecated-hint-rewrite-without-locality -w -deprecated-instance-without-locality -w -deprecated-typeclasses-transparency-without-locality -topfile file:///Users/pgiarrusso1/git/gDOT/dot-iris-make/theories/test_topfile.v

Suggested fix

Strip file:// or untitled: from the URL to get the raw path. This works even for unsaved files: we just need the path where the code would live if saved. EDIT: I'm not sure what I had in mind.