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

[lsp] Remove noop --std argument. #208

Merged
merged 1 commit into from
Jan 22, 2023
Merged

[lsp] Remove noop --std argument. #208

merged 1 commit into from
Jan 22, 2023

Conversation

ejgallego
Copy link
Owner

This argument was introduced very long time ago in the Lambdapi implementation as we were not fully LSP compliant, but now we are.

The argument itself has been disabled since a long time, and it misleading now; moreover we put it as default in package.json!!!

@ejgallego ejgallego added this to the 0.1.4 milestone Jan 21, 2023
Alizter
Alizter reviewed Jan 22, 2023
View reviewed changes
controller/coq_lsp.ml Outdated Show resolved Hide resolved
@ejgallego
Copy link
Owner Author

For a historical note, we needed this because in the first versions of the Lambdapi prototype, we sent the goals inside the diagnostics; this was not standard- compliant. We have now moved from that paradigm, and coq-lsp is fully standard compliant now TTBOMK.

If clients don't issue non-standard requests, they won't see any non-standard messages except for the $/ notifications, but these are legal by https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#dollarRequests:

Notification and requests whose methods start with ‘$/’ are messages which are protocol implementation dependent and might not be implementable in all clients or servers. For example if the server implementation uses a single threaded synchronous programming language then there is little a server can do to react to a $/cancelRequest notification. If a server or client receives notifications starting with ‘$/’ it is free to ignore the notification.

@ejgallego
[lsp] Remove noop --std argument.
bf4231e 
This argument was introduced very long time ago in the Lambdapi
implementation as we were not fully LSP compliant, but now we are.

The argument itself has been disabled since a long time, and it
misleading now; moreover we put it as default in `package.json`!!!
@Alizter
Copy link
Collaborator

Alizter commented Jan 22, 2023

Maybe getting rid of all the command line arguments will be for the better.

@ejgallego ejgallego merged commit 74b10c4 into main Jan 22, 2023
@ejgallego ejgallego deleted the no_std branch January 22, 2023 16:10
@ejgallego ejgallego mentioned this pull request Jan 29, 2023
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Jan 29, 2023
@ejgallego
[new release] coq-lsp (0.1.4+v8.16)
e05654b 
CHANGES:

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

 - Support for OCaml 4.11 (@ejgallego, ejgallego/coq-lsp#184)
 - The keybinding alt+enter in VSCode is now correctly scoped to be
   only active on Coq files (@artagnon, ejgallego/coq-lsp#188)
 - Support Unicode files (@ejgallego, ejgallego/coq-lsp#200, fixes ejgallego/coq-lsp#193, fixes ejgallego/coq-lsp#197)
 - The info view is now script enabled and does client-side
   rendering. It is also now bundled with esbuild as part of the build
   process (@artagnon, @ejgallego, ejgallego/coq-lsp#171)
 - The no-op `--std` argument to the `coq-lsp` binary has been
   removed, beware of your setup in the extension settings
   (@ejgallego, ejgallego/coq-lsp#208)
 - Settings for the VSCode extension are now categorized (@Alizter, ejgallego/coq-lsp#212)
 - `GoalAnswer`s now include the proof "stack" and better hypothesis
   information, changes are compatible with 0.1.3 `GoalAnswer` version
   (@ejgallego, ejgallego/coq-lsp#237)
 - Focus is now preserved when the info view pops up (@artagnon, ejgallego/coq-lsp#242,
   fixes ejgallego/coq-lsp#224)
 - In `_CoqProject`, `-impredicative-set` is now parsed correctly
   (@artagnon, ejgallego/coq-lsp#241)
 - InfoView is not written in React (@ejgallego, ejgallego/coq-lsp#223)
 - `debug` option in the client / protocol that will enable Coq's backtraces
   (@Alizter, @ejgallego, ejgallego/coq-lsp#217, ejgallego/coq-lsp#248)
 - Full document stats are now correctly computed on checking
   resumption, still cached sentences will display the cached timing
   tho (@ejgallego, ejgallego/coq-lsp#257)
 - Set Coq library name correctly (@ejgallego, ejgallego/coq-lsp#260)
 - `_CoqProject` file is now detected using LSP client `rootPath`
   (@ejgallego, ejgallego/coq-lsp#261)
 - Press `\` to trigger Unicode completion by the server. This
   behavior is configurable, with "off", "regular", and extended
   settings (@artagnon, @Alizter, ejgallego, ejgallego/coq-lsp#219).
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Jan 29, 2023
@ejgallego
[new release] coq-lsp (0.1.4+v8.16)
6554f83 
CHANGES:

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

 - Support for OCaml 4.11 (@ejgallego, ejgallego/coq-lsp#184)
 - The keybinding alt+enter in VSCode is now correctly scoped to be
   only active on Coq files (@artagnon, ejgallego/coq-lsp#188)
 - Support Unicode files (@ejgallego, ejgallego/coq-lsp#200, fixes ejgallego/coq-lsp#193, fixes ejgallego/coq-lsp#197)
 - The info view is now script enabled and does client-side
   rendering. It is also now bundled with esbuild as part of the build
   process (@artagnon, @ejgallego, ejgallego/coq-lsp#171)
 - The no-op `--std` argument to the `coq-lsp` binary has been
   removed, beware of your setup in the extension settings
   (@ejgallego, ejgallego/coq-lsp#208)
 - Settings for the VSCode extension are now categorized (@Alizter, ejgallego/coq-lsp#212)
 - `GoalAnswer`s now include the proof "stack" and better hypothesis
   information, changes are compatible with 0.1.3 `GoalAnswer` version
   (@ejgallego, ejgallego/coq-lsp#237)
 - Focus is now preserved when the info view pops up (@artagnon, ejgallego/coq-lsp#242,
   fixes ejgallego/coq-lsp#224)
 - In `_CoqProject`, `-impredicative-set` is now parsed correctly
   (@artagnon, ejgallego/coq-lsp#241)
 - InfoView is not written in React (@ejgallego, ejgallego/coq-lsp#223)
 - `debug` option in the client / protocol that will enable Coq's backtraces
   (@Alizter, @ejgallego, ejgallego/coq-lsp#217, ejgallego/coq-lsp#248)
 - Full document stats are now correctly computed on checking
   resumption, still cached sentences will display the cached timing
   tho (@ejgallego, ejgallego/coq-lsp#257)
 - Set Coq library name correctly (@ejgallego, ejgallego/coq-lsp#260)
 - `_CoqProject` file is now detected using LSP client `rootPath`
   (@ejgallego, ejgallego/coq-lsp#261)
 - You can press `\` to trigger Unicode completion by the server. This
   behavior is configurable, with "off", "regular", and "extended"
   settings (@artagnon, @Alizter, ejgallego, ejgallego/coq-lsp#219).
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Jan 29, 2023
@ejgallego
[new release] coq-lsp (0.1.4+v8.16)
1b58197 
CHANGES:

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

 - Support for OCaml 4.11 (@ejgallego, ejgallego/coq-lsp#184)
 - The keybinding alt+enter in VSCode is now correctly scoped to be
   only active on Coq files (@artagnon, ejgallego/coq-lsp#188)
 - Support Unicode files (@ejgallego, ejgallego/coq-lsp#200, fixes ejgallego/coq-lsp#193, fixes ejgallego/coq-lsp#197)
 - The info view is now script enabled and does client-side
   rendering. It is also now bundled with esbuild as part of the build
   process (@artagnon, @ejgallego, ejgallego/coq-lsp#171)
 - The no-op `--std` argument to the `coq-lsp` binary has been
   removed, beware of your setup in the extension settings
   (@ejgallego, ejgallego/coq-lsp#208)
 - Settings for the VSCode extension are now categorized (@Alizter, ejgallego/coq-lsp#212)
 - `GoalAnswer`s now include the proof "stack" and better hypothesis
   information, changes are compatible with 0.1.3 `GoalAnswer` version
   (@ejgallego, ejgallego/coq-lsp#237)
 - Focus is now preserved when the info view pops up (@artagnon, ejgallego/coq-lsp#242,
   fixes ejgallego/coq-lsp#224)
 - In `_CoqProject`, `-impredicative-set` is now parsed correctly
   (@artagnon, ejgallego/coq-lsp#241)
 - InfoView is not written in React (@ejgallego, ejgallego/coq-lsp#223)
 - `debug` option in the client / protocol that will enable Coq's backtraces
   (@Alizter, @ejgallego, ejgallego/coq-lsp#217, ejgallego/coq-lsp#248)
 - Full document stats are now correctly computed on checking
   resumption, still cached sentences will display the cached timing
   tho (@ejgallego, ejgallego/coq-lsp#257)
 - Set Coq library name correctly (@ejgallego, ejgallego/coq-lsp#260)
 - `_CoqProject` file is now detected using LSP client `rootPath`
   (@ejgallego, ejgallego/coq-lsp#261)
 - You can press `\` to trigger Unicode completion by the server. This
   behavior is configurable, with "off", "regular", and "extended"
   settings (@artagnon, @Alizter, ejgallego, ejgallego/coq-lsp#219).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Alizter Alizter Alizter approved these changes

Assignees
No one assigned
Labels
kind: cleanup part: lsp server
Projects
coq-lsp roadmap
Archived in project
Milestone
0.1.4
Development

Successfully merging this pull request may close these issues.
2 participants
@ejgallego @Alizter