Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Syntax error for "assert ... by ... " #281

Closed
orilahav opened this issue Feb 5, 2023 · 6 comments · Fixed by #287
Closed

Syntax error for "assert ... by ... " #281

orilahav opened this issue Feb 5, 2023 · 6 comments · Fixed by #287
Labels
kind: bug Something isn't working kind: upstream
Milestone
0.1.5

Comments

@orilahav
Copy link

orilahav commented Feb 5, 2023

assert ... by.. tactic generates "syntax error".
E.g. :

Lemma aaa : 1 = 0+1.
Proof.
assert (0+1 = 1) by (simpl; auto).
{ auto. }
Qed.
@Alizter
Copy link
Collaborator

Alizter commented Feb 5, 2023

Seems to work for me on both coq-lsp and CoqIDE. @orilahav Are you able to open other files? What is your lsp version / coq version?

@ejgallego
Copy link
Owner

ejgallego commented Feb 5, 2023 •
edited
Loading

@orilahav unfortunately this seems to be the problem that Coq parser gets indeed confused when opening multiple files; can you reproduce when you restart the server with just that file opened?

This bug causes some keywords such as by and |- to disappear from Coq :( :(

Next version will avoid this, maybe a good idea to release it ASAP.

@ejgallego ejgallego added kind: bug Something isn't working kind: upstream labels Feb 5, 2023
@orilahav
Copy link
Author

orilahav commented Feb 5, 2023

yes, this is unstable. I see this bug in long file, but the small example that failed before seems to work now.

coq 8.16.0 Formal proof management system
coq-lsp 0.1.4+v8.16 Language Server Protocol native server for

@ejgallego
Copy link
Owner

Thanks for the report @orilahav , this bug is fixed in Coq master, but I found a good workaround for the next release of coq-lsp, will try to update things ASAP.

For now if you get into this unfortunate error, the quickest way to solve it is keep just one .v file open, then run the "Restart coq-lsp server" command :( :(

@Alizter
Copy link
Collaborator

Alizter commented Feb 5, 2023

This is a bug in Coq that will be fixed in 8.17 which incorrectly backtracks when the parsing state is changed. So when one file loads something affecting the parsing of assert .. by .. the other files also see this since they are all related by backtracking.

@ejgallego
Copy link
Owner

@Alizter actually this is fixed for Coq 8.18, but I plan to try to backport the fix to 8.17, maybe we could even backport it to 8.16

@ejgallego ejgallego added this to the 0.1.5 milestone Feb 7, 2023
@ejgallego ejgallego mentioned this issue Feb 7, 2023
Merged
ejgallego added a commit that referenced this issue Feb 7, 2023
@ejgallego
[fleche] Reject opening multiple Coq documents for buggy Coq versions.
6dd0231 
Fixes #275 , #281

We use a heuristic in the fixed up branches as follows: if the Coq
version contains LSP, then we assume the fix has been backported.

That should work when doing `opam pin`.
@ejgallego ejgallego mentioned this issue Feb 15, 2023
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this issue Feb 15, 2023
@ejgallego
[new release] coq-lsp (0.1.5+8.16)
b7a2330 
CHANGES:

---------------------

 - Fix a bug when trying to complete in an empty file (@ejgallego,
   ejgallego/coq-lsp#270)
 - Fix a bug with the position reported by the `$/coq/fileProgress`
   notification
 - Fix messages panel rendering after the port to React (@ejgallego,
   ejgallego/coq-lsp#272)
 - Fix non-compliance with LSP range type due to extra `offset` field
   (@ejgallego, ejgallego/coq-lsp#271)
 - The goal display now numbers goals starting with 1 instead of 0
   (@artagnon, ejgallego/coq-lsp#277, report by Hugo Herbelin)
 - Markdown Coq code blocks now must specify "coq" as a language
   (@ejgallego, ejgallego/coq-lsp#280)
 - Server is now more strict w.r.t. what URIs it will accept for
   documents, see protocol documentation (@ejgallego, ejgallego/coq-lsp#286, reported
   by Alex Sanchez-Stern)
 - Hypotheses with bodies are now correctly displayed (@ejgallego,
   ejgallego/coq-lsp#296, fixes ejgallego/coq-lsp#293, report by Ali Caglayan)
 - `coq-lsp` incorrectly required the optional `rootPath`
   initialization parameter, moreover it ignored `rootUri` if present
   which goes against the LSP spec (@ejgallego, ejgallego/coq-lsp#295, report by Alex
   Sanchez-Stern)
 - `coq-lsp` will now reject opening multiple files when the
   underlying Coq version is buggy (@ejgallego, fixes ejgallego/coq-lsp#275, fixes
   ejgallego/coq-lsp#281)
 - Fix bug when parsing client option for unicode completion
   (@ejgallego ejgallego/coq-lsp#301)
 - Support unicode characters in filenames (@artagnon, ejgallego/coq-lsp#302)
 - Stop checking documents after a maximum number of errors,
   user-configurable (by default 150) (@ejgallego, ejgallego/coq-lsp#303)
 - Coq Markdown files (.mv extension) are now highlighted properly
   using both Coq and Markdown syntax rules (@4ever2, ejgallego/coq-lsp#307)
 - Goal view now supports find (@Alizter, ejgallego/coq-lsp#309, closes ejgallego/coq-lsp#305)
 - coq-lsp now understands a basic version of Coq Waterproof files
   (.wpn) Note that we don't associate to them by default, as to allow
   the waterproof extension to take over the files (@ejgallego, ejgallego/coq-lsp#306)
 - URI validation is now more strict, and some further bugs should be
   solved; note still this can be an issue on some client settings
   (@ejgallego, ejgallego/coq-lsp#313, fixes ejgallego/coq-lsp#187)
 - Display Coq info and debug messages in info panel (@ejgallego,
   ejgallego/coq-lsp#314, fixes ejgallego/coq-lsp#308)
 - Goal display handles background goals better, showing preview,
   goals stack, and focusing information (@ejgallego, ejgallego/coq-lsp#290, fixes
   ejgallego/coq-lsp#288, fixes ejgallego/coq-lsp#304, based on jsCoq code by Shachar Itzhaky)
 - Warnings are now printed in the info view messages panel
   (@ejgallego, ejgallego/coq-lsp#315, fixes ejgallego/coq-lsp#195)
 - Info protocol messages now have location and level
   (@ejgallego, ejgallego/coq-lsp#315)
 - Warnings are not printed in the info view messages panel
   (@ejgallego, #, fixes ejgallego/coq-lsp#195)
 - Improved `documentSymbol` return type for newer `DocumentSymbol[]`
   hierarchical symbol support. This means that sections and modules
   will now be properly represented, as well as constructors for
   inductive types, projections for records, etc...  (@ejgallego,
   ejgallego/coq-lsp#174, fixes ejgallego/coq-lsp#121, ejgallego/coq-lsp#122)
 - [internal] Error recovery can now execute full Coq commands as to
   amend states, required for ejgallego/coq-lsp#319 (@ejallego, ejgallego/coq-lsp#320)
 - Auto-admit the previous bullet goal when a new bullet cannot be
   opened due to an unsolved previous bullet. This also works for {}
   focusing operators. This is very useful when navigating bulleted
   proofs (@ejgallego, @Alizter, ejgallego/coq-lsp#319, fixes ejgallego/coq-lsp#300)
 - Store Ast.Info.t incrementally (@ejgallego, ejgallego/coq-lsp#337, fixes ejgallego/coq-lsp#316)
 - Basic jump to definition support; due to lack of workspace
   metadata, this only works inside the same file (@ejgallego, ejgallego/coq-lsp#318)
 - Show type of identifiers at point on hover (@ejgallego, ejgallego/coq-lsp#321, cc:
   ejgallego/coq-lsp#164)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: bug Something isn't working kind: upstream
Projects
None yet
Milestone
0.1.5
Development

Successfully merging a pull request may close this issue.

[fleche] Reject opening multiple Coq documents for buggy Coq versions. ejgallego/coq-lsp
3 participants
@ejgallego @Alizter @orilahav