-
Notifications
You must be signed in to change notification settings - Fork 65
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
vscoq passes incorrect -topfile
argument
#278
Milestone
Comments
Blaisorblade
added a commit
to Blaisorblade/vscoq
that referenced
this issue
Feb 10, 2023
This also allows stepping through unsaved files; before this patch, we passed `-topfile untitled:Untitled-1`, which failed with: ``` coqtop-stderr: Error: Invalid character ':' in identifier "untitled:Untitled-1". ```
Blaisorblade
added a commit
to Blaisorblade/vscoq
that referenced
this issue
Feb 10, 2023
This also allows stepping through unsaved files; before this patch, we passed `-topfile untitled:Untitled-1`, which failed with: ``` coqtop-stderr: Error: Invalid character ':' in identifier "untitled:Untitled-1". ```
Blaisorblade
added a commit
to Blaisorblade/vscoq
that referenced
this issue
Feb 11, 2023
This also allows stepping through unsaved files; before this patch, we passed `-topfile untitled:Untitled-1`, which failed with: ``` coqtop-stderr: Error: Invalid character ':' in identifier "untitled:Untitled-1". ```
Blaisorblade
added a commit
to Blaisorblade/vscoq
that referenced
this issue
Apr 11, 2023
This also allows stepping through unsaved files; before this patch, we passed `-topfile untitled:Untitled-1`, which failed with: ``` coqtop-stderr: Error: Invalid character ':' in identifier "untitled:Untitled-1". ```
4ever2
pushed a commit
to 4ever2/vscoq
that referenced
this issue
Sep 12, 2023
This also allows stepping through unsaved files; before this patch, we passed `-topfile untitled:Untitled-1`, which failed with: ``` coqtop-stderr: Error: Invalid character ':' in identifier "untitled:Untitled-1". ```
thery
added a commit
that referenced
this issue
Sep 13, 2023
[VsCoq1] Fix #278: pass correct `-topfile` argument
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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
, andtest_topfile.v
is the following: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:
Suggested fix
Strip
file://
oruntitled:
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.The text was updated successfully, but these errors were encountered: