[workspace] use rootPath to detect _CoqProject file.
#261
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
ejgallego
force-pushed
the
fix_coqproject_detection
branch
from
862d32b to
3f6d7ff
Compare
This is needed in quite a few cases, thus a fix.
ejgallego
force-pushed
the
fix_coqproject_detection
branch
from
3f6d7ff to
0ad2339
Compare
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this pull request
Jan 29, 2023
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
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
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
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This is needed in quite a few cases, thus a fix.