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

Fix typo in -impredicative-set parsing #241

Merged
merged 2 commits into from
Jan 26, 2023
Merged

Fix typo in -impredicative-set parsing #241

merged 2 commits into from
Jan 26, 2023

Conversation

artagnon
Copy link
Collaborator

No description provided.

ejgallego
ejgallego reviewed Jan 25, 2023
View reviewed changes
ejgallego
ejgallego requested changes Jan 25, 2023
View reviewed changes
Copy link
Owner

@ejgallego ejgallego left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks a lot for the fix, however the unrelated change needs to be removed (or an issue opened) as it is a real TODO.

@ejgallego ejgallego added this to the 0.1.4 milestone Jan 25, 2023
@ejgallego
Copy link
Owner

I guess a changelog would be also useful, users may wonder why it was not working before.

@ejgallego
Copy link
Owner

Also we could add an entry for this in examples (or tests very soon I hope!)

@artagnon
Copy link
Collaborator Author

We can't add an example, as it requires a _CoqProject to be at the root of the repository.

@artagnon artagnon requested a review from ejgallego January 26, 2023 11:08
@ejgallego
Copy link
Owner

We can't add an example, as it requires a _CoqProject to be at the root of the repository.

I guess we can add subdirs in example, let's discuss about this in person as it is really related to #15

@ejgallego ejgallego merged commit b3e511c into ejgallego:main Jan 26, 2023
@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

@ejgallego ejgallego ejgallego approved these changes

Assignees
No one assigned
Labels
kind: fix needs: changes entry
Projects
coq-lsp roadmap
Archived in project
Milestone
0.1.4
Development

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