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

[server] URI validation #187

Closed
ejgallego opened this issue Jan 17, 2023 · 0 comments · Fixed by #313 or ocaml/opam-repository#23319
Closed

[server] URI validation #187

ejgallego opened this issue Jan 17, 2023 · 0 comments · Fixed by #313 or ocaml/opam-repository#23319
Milestone
0.1.5

Comments

@ejgallego
Copy link
Owner

This is helpful in case clients do a mistake, as otherwise the error message will result confusing.
@ejgallego ejgallego modified the milestones: 0.1.4, 0.1.5 Jan 17, 2023
@ejgallego ejgallego modified the milestones: 0.1.5, 0.1.6 Jan 28, 2023
@ejgallego ejgallego mentioned this issue Feb 7, 2023
Merged
@ejgallego ejgallego modified the milestones: 0.1.6, 0.1.5 Feb 9, 2023
ejgallego added a commit that referenced this issue Feb 9, 2023
@ejgallego
[lsp] Abstract URI type, improve URI validation.
760cbde 
This should help preventing many issues that can happen due to bad
URIs; still quite a bit of work to do here, but the code overall,
while a bit uglier, seems safer.

Fixes #187
@ejgallego ejgallego mentioned this issue Feb 9, 2023
Merged
ejgallego added a commit that referenced this issue Feb 9, 2023
@ejgallego
[lsp] Abstract URI type, improve URI validation.
e3d4442 
This should help preventing many issues that can happen due to bad
URIs; still quite a bit of work to do here, but the code overall,
while a bit uglier, seems safer.

Fixes #187
ejgallego added a commit that referenced this issue Feb 9, 2023
@ejgallego
[lsp] Abstract URI type, improve URI validation.
b681177 
This should help preventing many issues that can happen due to bad
URIs; still quite a bit of work to do here, but the code overall,
while a bit uglier, seems safer.

Fixes #187
ejgallego added a commit that referenced this issue Feb 9, 2023
@ejgallego
[lsp] Abstract URI type, improve URI validation.
b04015a 
This should help preventing many issues that can happen due to bad
URIs; still quite a bit of work to do here, but the code overall,
while a bit uglier, seems safer.

Fixes #187
@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
None yet
Projects
coq-lsp roadmap
Archived in project
Milestone
0.1.5
1 participant
@ejgallego