Multiple warning display options in _CoqProject are not handled correctly #540
Labels
Milestone
Comments
|
Hi @mituharu , indeed that was a silly bug, Coq's warnings API is a bit confusing for me. Will be fixed very soon, thanks a lot for the very careful bug report. |
|
I'd be nice to add this to the test suite. |
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this issue
Oct 25, 2023
CHANGES: ------------------------------- - Update VSCode client dependencies, should bring some performance improvements to goal pretty printing (@ejgallego, ejgallego/coq-lsp#530) - Update goal display colors for light mode so they are actually readable now. (@bhaktishh, ejgallego/coq-lsp#539, fixes ejgallego/coq-lsp#532) - Added link to Python coq-lsp client by Pedro Carrot and Nuno Saavedra (@Nfsaavedra, ejgallego/coq-lsp#536) - Properly concatenate warnings from _CoqProject (@ejgallego, reported by @mituharu, ejgallego/coq-lsp#541, fixes ejgallego/coq-lsp#540) - Fix broken `coq/saveVo` and `coq/getDocument` requests due to a parsing problem with extra fields in their requests (@ejgallego, ejgallego/coq-lsp#547, reported by @Zimmi48) - `fcc` now understands the `--coqlib`, `--coqcorelib`, `--ocamlpath`, `-Q` and `-R` arguments (@ejgallego, ejgallego/coq-lsp#555) - Describe findlib status in `Workspace.describe`, which is printed in the output windows (@ejgallego, ejgallego/coq-lsp#556) - `coq-lsp` plugin loader will now be strict in case of a plugin failure, the previous loose behavior was more convenient for the early releases, but it doesn't make sense now and made things pretty hard to debug on the Windows installer (@ejgallego, ejgallego/coq-lsp#557) - Add pointers to Windows installers (@ejgallego, ejgallego/coq-lsp#559) - Recognize `Goal` and `Definition $id : ... .` as proof starters (@ejgallego, ejgallego/coq-lsp#561, reported by @Zimmi48, fixes ejgallego/coq-lsp#548) - Provide basic notation information on hover. This is intended for people to build their own more refined notation feedback systems (@ejgallego, ejgallego/coq-lsp#562) - Hover request can now be extended by plugins (@ejgallego, ejgallego/coq-lsp#562) - Updated LSP and JS client libs, notably to vscode-languageclient 9 (@ejgallego, ejgallego/coq-lsp#565) - Implement a LIFO document scheduler, this is heavier in the background as more documents will be checked, but provides a few usability improvements (@ejgallego, ejgallego/coq-lsp#566, fixes ejgallego/coq-lsp#563, reported by Ali Caglayan) - New lexical qed detection error recovery rule; this makes a very large usability difference in practice when editing inside proofs. (@ejgallego, ejgallego/coq-lsp#567, fixes ejgallego/coq-lsp#33) - `coq-lsp` is now supported by the `coq-nix-toolbox` (@Zimmi48, @CohenCyril, ejgallego/coq-lsp#572, via coq-community/coq-nix-toolbox#164 ) - Support for `-rifrom` in `_CoqProject` and in command line (`--rifrom`). Thanks to Lasse Blaauwbroek for the report. (@ejgallego, ejgallego/coq-lsp#581, fixes ejgallego/coq-lsp#579) - Export Query Goals API in VSCode client; this way other extensions can implement their own commands that query Coq goals (@amblafont, @ejgallego, ejgallego/coq-lsp#576, closes ejgallego/coq-lsp#558) - New `pretac` field for preprocessing of goals with a tactic using speculative execution, this is experimental for now (@amblafont, @ejgallego, ejgallego/coq-lsp#573, helps with ejgallego/coq-lsp#558) - Implement `textDocument/selectionRange` request, that will return the range of the Coq sentence underlying the cursor. In VSCode, this is triggered by the "Expand Selection" command. The implementation is partial: we only take into account the first position, and we only return a single range (Coq sentence) without parents. (@ejgallego, ejgallego/coq-lsp#582) - Be more robust to mixed-separator windows paths in workspace detection (@ejgallego, ejgallego/coq-lsp#583, fixes ejgallego/coq-lsp#569) - Adjust printing breaks in error and message panels (@ejgallego, @Alizter, ejgallego/coq-lsp#586, fixes ejgallego/coq-lsp#457 , fixes ejgallego/coq-lsp#458 , fixes ejgallego/coq-lsp#571)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this issue
Oct 25, 2023
CHANGES: ------------------------------- - Update VSCode client dependencies, should bring some performance improvements to goal pretty printing (@ejgallego, ejgallego/coq-lsp#530) - Update goal display colors for light mode so they are actually readable now. (@bhaktishh, ejgallego/coq-lsp#539, fixes ejgallego/coq-lsp#532) - Added link to Python coq-lsp client by Pedro Carrot and Nuno Saavedra (@Nfsaavedra, ejgallego/coq-lsp#536) - Properly concatenate warnings from _CoqProject (@ejgallego, reported by @mituharu, ejgallego/coq-lsp#541, fixes ejgallego/coq-lsp#540) - Fix broken `coq/saveVo` and `coq/getDocument` requests due to a parsing problem with extra fields in their requests (@ejgallego, ejgallego/coq-lsp#547, reported by @Zimmi48) - `fcc` now understands the `--coqlib`, `--coqcorelib`, `--ocamlpath`, `-Q` and `-R` arguments (@ejgallego, ejgallego/coq-lsp#555) - Describe findlib status in `Workspace.describe`, which is printed in the output windows (@ejgallego, ejgallego/coq-lsp#556) - `coq-lsp` plugin loader will now be strict in case of a plugin failure, the previous loose behavior was more convenient for the early releases, but it doesn't make sense now and made things pretty hard to debug on the Windows installer (@ejgallego, ejgallego/coq-lsp#557) - Add pointers to Windows installers (@ejgallego, ejgallego/coq-lsp#559) - Recognize `Goal` and `Definition $id : ... .` as proof starters (@ejgallego, ejgallego/coq-lsp#561, reported by @Zimmi48, fixes ejgallego/coq-lsp#548) - Provide basic notation information on hover. This is intended for people to build their own more refined notation feedback systems (@ejgallego, ejgallego/coq-lsp#562) - Hover request can now be extended by plugins (@ejgallego, ejgallego/coq-lsp#562) - Updated LSP and JS client libs, notably to vscode-languageclient 9 (@ejgallego, ejgallego/coq-lsp#565) - Implement a LIFO document scheduler, this is heavier in the background as more documents will be checked, but provides a few usability improvements (@ejgallego, ejgallego/coq-lsp#566, fixes ejgallego/coq-lsp#563, reported by Ali Caglayan) - New lexical qed detection error recovery rule; this makes a very large usability difference in practice when editing inside proofs. (@ejgallego, ejgallego/coq-lsp#567, fixes ejgallego/coq-lsp#33) - `coq-lsp` is now supported by the `coq-nix-toolbox` (@Zimmi48, @CohenCyril, ejgallego/coq-lsp#572, via coq-community/coq-nix-toolbox#164 ) - Support for `-rifrom` in `_CoqProject` and in command line (`--rifrom`). Thanks to Lasse Blaauwbroek for the report. (@ejgallego, ejgallego/coq-lsp#581, fixes ejgallego/coq-lsp#579) - Export Query Goals API in VSCode client; this way other extensions can implement their own commands that query Coq goals (@amblafont, @ejgallego, ejgallego/coq-lsp#576, closes ejgallego/coq-lsp#558) - New `pretac` field for preprocessing of goals with a tactic using speculative execution, this is experimental for now (@amblafont, @ejgallego, ejgallego/coq-lsp#573, helps with ejgallego/coq-lsp#558) - Implement `textDocument/selectionRange` request, that will return the range of the Coq sentence underlying the cursor. In VSCode, this is triggered by the "Expand Selection" command. The implementation is partial: we only take into account the first position, and we only return a single range (Coq sentence) without parents. (@ejgallego, ejgallego/coq-lsp#582) - Be more robust to mixed-separator windows paths in workspace detection (@ejgallego, ejgallego/coq-lsp#583, fixes ejgallego/coq-lsp#569) - Adjust printing breaks in error and message panels (@ejgallego, @Alizter, ejgallego/coq-lsp#586, fixes ejgallego/coq-lsp#457 , fixes ejgallego/coq-lsp#458 , fixes ejgallego/coq-lsp#571)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this issue
Oct 25, 2023
CHANGES: ------------------------------- - Update VSCode client dependencies, should bring some performance improvements to goal pretty printing (@ejgallego, ejgallego/coq-lsp#530) - Update goal display colors for light mode so they are actually readable now. (@bhaktishh, ejgallego/coq-lsp#539, fixes ejgallego/coq-lsp#532) - Added link to Python coq-lsp client by Pedro Carrot and Nuno Saavedra (@Nfsaavedra, ejgallego/coq-lsp#536) - Properly concatenate warnings from _CoqProject (@ejgallego, reported by @mituharu, ejgallego/coq-lsp#541, fixes ejgallego/coq-lsp#540) - Fix broken `coq/saveVo` and `coq/getDocument` requests due to a parsing problem with extra fields in their requests (@ejgallego, ejgallego/coq-lsp#547, reported by @Zimmi48) - `fcc` now understands the `--coqlib`, `--coqcorelib`, `--ocamlpath`, `-Q` and `-R` arguments (@ejgallego, ejgallego/coq-lsp#555) - Describe findlib status in `Workspace.describe`, which is printed in the output windows (@ejgallego, ejgallego/coq-lsp#556) - `coq-lsp` plugin loader will now be strict in case of a plugin failure, the previous loose behavior was more convenient for the early releases, but it doesn't make sense now and made things pretty hard to debug on the Windows installer (@ejgallego, ejgallego/coq-lsp#557) - Add pointers to Windows installers (@ejgallego, ejgallego/coq-lsp#559) - Recognize `Goal` and `Definition $id : ... .` as proof starters (@ejgallego, ejgallego/coq-lsp#561, reported by @Zimmi48, fixes ejgallego/coq-lsp#548) - Provide basic notation information on hover. This is intended for people to build their own more refined notation feedback systems (@ejgallego, ejgallego/coq-lsp#562) - Hover request can now be extended by plugins (@ejgallego, ejgallego/coq-lsp#562) - Updated LSP and JS client libs, notably to vscode-languageclient 9 (@ejgallego, ejgallego/coq-lsp#565) - Implement a LIFO document scheduler, this is heavier in the background as more documents will be checked, but provides a few usability improvements (@ejgallego, ejgallego/coq-lsp#566, fixes ejgallego/coq-lsp#563, reported by Ali Caglayan) - New lexical qed detection error recovery rule; this makes a very large usability difference in practice when editing inside proofs. (@ejgallego, ejgallego/coq-lsp#567, fixes ejgallego/coq-lsp#33) - `coq-lsp` is now supported by the `coq-nix-toolbox` (@Zimmi48, @CohenCyril, ejgallego/coq-lsp#572, via coq-community/coq-nix-toolbox#164 ) - Support for `-rifrom` in `_CoqProject` and in command line (`--rifrom`). Thanks to Lasse Blaauwbroek for the report. (@ejgallego, ejgallego/coq-lsp#581, fixes ejgallego/coq-lsp#579) - Export Query Goals API in VSCode client; this way other extensions can implement their own commands that query Coq goals (@amblafont, @ejgallego, ejgallego/coq-lsp#576, closes ejgallego/coq-lsp#558) - New `pretac` field for preprocessing of goals with a tactic using speculative execution, this is experimental for now (@amblafont, @ejgallego, ejgallego/coq-lsp#573, helps with ejgallego/coq-lsp#558) - Implement `textDocument/selectionRange` request, that will return the range of the Coq sentence underlying the cursor. In VSCode, this is triggered by the "Expand Selection" command. The implementation is partial: we only take into account the first position, and we only return a single range (Coq sentence) without parents. (@ejgallego, ejgallego/coq-lsp#582) - Be more robust to mixed-separator windows paths in workspace detection (@ejgallego, ejgallego/coq-lsp#583, fixes ejgallego/coq-lsp#569) - Adjust printing breaks in error and message panels (@ejgallego, @Alizter, ejgallego/coq-lsp#586, fixes ejgallego/coq-lsp#457 , fixes ejgallego/coq-lsp#458 , fixes ejgallego/coq-lsp#571)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this issue
Feb 5, 2024
CHANGES: ------------------------------- - Update VSCode client dependencies, should bring some performance improvements to goal pretty printing (@ejgallego, ejgallego/coq-lsp#530) - Update goal display colors for light mode so they are actually readable now. (@bhaktishh, ejgallego/coq-lsp#539, fixes ejgallego/coq-lsp#532) - Added link to Python coq-lsp client by Pedro Carrot and Nuno Saavedra (@Nfsaavedra, ejgallego/coq-lsp#536) - Properly concatenate warnings from _CoqProject (@ejgallego, reported by @mituharu, ejgallego/coq-lsp#541, fixes ejgallego/coq-lsp#540) - Fix broken `coq/saveVo` and `coq/getDocument` requests due to a parsing problem with extra fields in their requests (@ejgallego, ejgallego/coq-lsp#547, reported by @Zimmi48) - `fcc` now understands the `--coqlib`, `--coqcorelib`, `--ocamlpath`, `-Q` and `-R` arguments (@ejgallego, ejgallego/coq-lsp#555) - Describe findlib status in `Workspace.describe`, which is printed in the output windows (@ejgallego, ejgallego/coq-lsp#556) - `coq-lsp` plugin loader will now be strict in case of a plugin failure, the previous loose behavior was more convenient for the early releases, but it doesn't make sense now and made things pretty hard to debug on the Windows installer (@ejgallego, ejgallego/coq-lsp#557) - Add pointers to Windows installers (@ejgallego, ejgallego/coq-lsp#559) - Recognize `Goal` and `Definition $id : ... .` as proof starters (@ejgallego, ejgallego/coq-lsp#561, reported by @Zimmi48, fixes ejgallego/coq-lsp#548) - Provide basic notation information on hover. This is intended for people to build their own more refined notation feedback systems (@ejgallego, ejgallego/coq-lsp#562) - Hover request can now be extended by plugins (@ejgallego, ejgallego/coq-lsp#562) - Updated LSP and JS client libs, notably to vscode-languageclient 9 (@ejgallego, ejgallego/coq-lsp#565) - Implement a LIFO document scheduler, this is heavier in the background as more documents will be checked, but provides a few usability improvements (@ejgallego, ejgallego/coq-lsp#566, fixes ejgallego/coq-lsp#563, reported by Ali Caglayan) - New lexical qed detection error recovery rule; this makes a very large usability difference in practice when editing inside proofs. (@ejgallego, ejgallego/coq-lsp#567, fixes ejgallego/coq-lsp#33) - `coq-lsp` is now supported by the `coq-nix-toolbox` (@Zimmi48, @CohenCyril, ejgallego/coq-lsp#572, via coq-community/coq-nix-toolbox#164 ) - Support for `-rifrom` in `_CoqProject` and in command line (`--rifrom`). Thanks to Lasse Blaauwbroek for the report. (@ejgallego, ejgallego/coq-lsp#581, fixes ejgallego/coq-lsp#579) - Export Query Goals API in VSCode client; this way other extensions can implement their own commands that query Coq goals (@amblafont, @ejgallego, ejgallego/coq-lsp#576, closes ejgallego/coq-lsp#558) - New `pretac` field for preprocessing of goals with a tactic using speculative execution, this is experimental for now (@amblafont, @ejgallego, ejgallego/coq-lsp#573, helps with ejgallego/coq-lsp#558) - Implement `textDocument/selectionRange` request, that will return the range of the Coq sentence underlying the cursor. In VSCode, this is triggered by the "Expand Selection" command. The implementation is partial: we only take into account the first position, and we only return a single range (Coq sentence) without parents. (@ejgallego, ejgallego/coq-lsp#582) - Be more robust to mixed-separator windows paths in workspace detection (@ejgallego, ejgallego/coq-lsp#583, fixes ejgallego/coq-lsp#569) - Adjust printing breaks in error and message panels (@ejgallego, @Alizter, ejgallego/coq-lsp#586, fixes ejgallego/coq-lsp#457 , fixes ejgallego/coq-lsp#458 , fixes ejgallego/coq-lsp#571)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this issue
Feb 6, 2024
CHANGES: ------------------------------- - Update VSCode client dependencies, should bring some performance improvements to goal pretty printing (@ejgallego, ejgallego/coq-lsp#530) - Update goal display colors for light mode so they are actually readable now. (@bhaktishh, ejgallego/coq-lsp#539, fixes ejgallego/coq-lsp#532) - Added link to Python coq-lsp client by Pedro Carrot and Nuno Saavedra (@Nfsaavedra, ejgallego/coq-lsp#536) - Properly concatenate warnings from _CoqProject (@ejgallego, reported by @mituharu, ejgallego/coq-lsp#541, fixes ejgallego/coq-lsp#540) - Fix broken `coq/saveVo` and `coq/getDocument` requests due to a parsing problem with extra fields in their requests (@ejgallego, ejgallego/coq-lsp#547, reported by @Zimmi48) - `fcc` now understands the `--coqlib`, `--coqcorelib`, `--ocamlpath`, `-Q` and `-R` arguments (@ejgallego, ejgallego/coq-lsp#555) - Describe findlib status in `Workspace.describe`, which is printed in the output windows (@ejgallego, ejgallego/coq-lsp#556) - `coq-lsp` plugin loader will now be strict in case of a plugin failure, the previous loose behavior was more convenient for the early releases, but it doesn't make sense now and made things pretty hard to debug on the Windows installer (@ejgallego, ejgallego/coq-lsp#557) - Add pointers to Windows installers (@ejgallego, ejgallego/coq-lsp#559) - Recognize `Goal` and `Definition $id : ... .` as proof starters (@ejgallego, ejgallego/coq-lsp#561, reported by @Zimmi48, fixes ejgallego/coq-lsp#548) - Provide basic notation information on hover. This is intended for people to build their own more refined notation feedback systems (@ejgallego, ejgallego/coq-lsp#562) - Hover request can now be extended by plugins (@ejgallego, ejgallego/coq-lsp#562) - Updated LSP and JS client libs, notably to vscode-languageclient 9 (@ejgallego, ejgallego/coq-lsp#565) - Implement a LIFO document scheduler, this is heavier in the background as more documents will be checked, but provides a few usability improvements (@ejgallego, ejgallego/coq-lsp#566, fixes ejgallego/coq-lsp#563, reported by Ali Caglayan) - New lexical qed detection error recovery rule; this makes a very large usability difference in practice when editing inside proofs. (@ejgallego, ejgallego/coq-lsp#567, fixes ejgallego/coq-lsp#33) - `coq-lsp` is now supported by the `coq-nix-toolbox` (@Zimmi48, @CohenCyril, ejgallego/coq-lsp#572, via coq-community/coq-nix-toolbox#164 ) - Support for `-rifrom` in `_CoqProject` and in command line (`--rifrom`). Thanks to Lasse Blaauwbroek for the report. (@ejgallego, ejgallego/coq-lsp#581, fixes ejgallego/coq-lsp#579) - Export Query Goals API in VSCode client; this way other extensions can implement their own commands that query Coq goals (@amblafont, @ejgallego, ejgallego/coq-lsp#576, closes ejgallego/coq-lsp#558) - New `pretac` field for preprocessing of goals with a tactic using speculative execution, this is experimental for now (@amblafont, @ejgallego, ejgallego/coq-lsp#573, helps with ejgallego/coq-lsp#558) - Implement `textDocument/selectionRange` request, that will return the range of the Coq sentence underlying the cursor. In VSCode, this is triggered by the "Expand Selection" command. The implementation is partial: we only take into account the first position, and we only return a single range (Coq sentence) without parents. (@ejgallego, ejgallego/coq-lsp#582) - Be more robust to mixed-separator windows paths in workspace detection (@ejgallego, ejgallego/coq-lsp#583, fixes ejgallego/coq-lsp#569) - Adjust printing breaks in error and message panels (@ejgallego, @Alizter, ejgallego/coq-lsp#586, fixes ejgallego/coq-lsp#457 , fixes ejgallego/coq-lsp#458 , fixes ejgallego/coq-lsp#571)
nberth
pushed a commit
to nberth/opam-repository
that referenced
this issue
Jun 18, 2024
CHANGES: ------------------------------- - Update VSCode client dependencies, should bring some performance improvements to goal pretty printing (@ejgallego, ejgallego/coq-lsp#530) - Update goal display colors for light mode so they are actually readable now. (@bhaktishh, ejgallego/coq-lsp#539, fixes ejgallego/coq-lsp#532) - Added link to Python coq-lsp client by Pedro Carrot and Nuno Saavedra (@Nfsaavedra, ejgallego/coq-lsp#536) - Properly concatenate warnings from _CoqProject (@ejgallego, reported by @mituharu, ejgallego/coq-lsp#541, fixes ejgallego/coq-lsp#540) - Fix broken `coq/saveVo` and `coq/getDocument` requests due to a parsing problem with extra fields in their requests (@ejgallego, ejgallego/coq-lsp#547, reported by @Zimmi48) - `fcc` now understands the `--coqlib`, `--coqcorelib`, `--ocamlpath`, `-Q` and `-R` arguments (@ejgallego, ejgallego/coq-lsp#555) - Describe findlib status in `Workspace.describe`, which is printed in the output windows (@ejgallego, ejgallego/coq-lsp#556) - `coq-lsp` plugin loader will now be strict in case of a plugin failure, the previous loose behavior was more convenient for the early releases, but it doesn't make sense now and made things pretty hard to debug on the Windows installer (@ejgallego, ejgallego/coq-lsp#557) - Add pointers to Windows installers (@ejgallego, ejgallego/coq-lsp#559) - Recognize `Goal` and `Definition $id : ... .` as proof starters (@ejgallego, ejgallego/coq-lsp#561, reported by @Zimmi48, fixes ejgallego/coq-lsp#548) - Provide basic notation information on hover. This is intended for people to build their own more refined notation feedback systems (@ejgallego, ejgallego/coq-lsp#562) - Hover request can now be extended by plugins (@ejgallego, ejgallego/coq-lsp#562) - Updated LSP and JS client libs, notably to vscode-languageclient 9 (@ejgallego, ejgallego/coq-lsp#565) - Implement a LIFO document scheduler, this is heavier in the background as more documents will be checked, but provides a few usability improvements (@ejgallego, ejgallego/coq-lsp#566, fixes ejgallego/coq-lsp#563, reported by Ali Caglayan) - New lexical qed detection error recovery rule; this makes a very large usability difference in practice when editing inside proofs. (@ejgallego, ejgallego/coq-lsp#567, fixes ejgallego/coq-lsp#33) - `coq-lsp` is now supported by the `coq-nix-toolbox` (@Zimmi48, @CohenCyril, ejgallego/coq-lsp#572, via coq-community/coq-nix-toolbox#164 ) - Support for `-rifrom` in `_CoqProject` and in command line (`--rifrom`). Thanks to Lasse Blaauwbroek for the report. (@ejgallego, ejgallego/coq-lsp#581, fixes ejgallego/coq-lsp#579) - Export Query Goals API in VSCode client; this way other extensions can implement their own commands that query Coq goals (@amblafont, @ejgallego, ejgallego/coq-lsp#576, closes ejgallego/coq-lsp#558) - New `pretac` field for preprocessing of goals with a tactic using speculative execution, this is experimental for now (@amblafont, @ejgallego, ejgallego/coq-lsp#573, helps with ejgallego/coq-lsp#558) - Implement `textDocument/selectionRange` request, that will return the range of the Coq sentence underlying the cursor. In VSCode, this is triggered by the "Expand Selection" command. The implementation is partial: we only take into account the first position, and we only return a single range (Coq sentence) without parents. (@ejgallego, ejgallego/coq-lsp#582) - Be more robust to mixed-separator windows paths in workspace detection (@ejgallego, ejgallego/coq-lsp#583, fixes ejgallego/coq-lsp#569) - Adjust printing breaks in error and message panels (@ejgallego, @Alizter, ejgallego/coq-lsp#586, fixes ejgallego/coq-lsp#457 , fixes ejgallego/coq-lsp#458 , fixes ejgallego/coq-lsp#571)
nberth
pushed a commit
to nberth/opam-repository
that referenced
this issue
Jun 18, 2024
CHANGES: ------------------------------- - Update VSCode client dependencies, should bring some performance improvements to goal pretty printing (@ejgallego, ejgallego/coq-lsp#530) - Update goal display colors for light mode so they are actually readable now. (@bhaktishh, ejgallego/coq-lsp#539, fixes ejgallego/coq-lsp#532) - Added link to Python coq-lsp client by Pedro Carrot and Nuno Saavedra (@Nfsaavedra, ejgallego/coq-lsp#536) - Properly concatenate warnings from _CoqProject (@ejgallego, reported by @mituharu, ejgallego/coq-lsp#541, fixes ejgallego/coq-lsp#540) - Fix broken `coq/saveVo` and `coq/getDocument` requests due to a parsing problem with extra fields in their requests (@ejgallego, ejgallego/coq-lsp#547, reported by @Zimmi48) - `fcc` now understands the `--coqlib`, `--coqcorelib`, `--ocamlpath`, `-Q` and `-R` arguments (@ejgallego, ejgallego/coq-lsp#555) - Describe findlib status in `Workspace.describe`, which is printed in the output windows (@ejgallego, ejgallego/coq-lsp#556) - `coq-lsp` plugin loader will now be strict in case of a plugin failure, the previous loose behavior was more convenient for the early releases, but it doesn't make sense now and made things pretty hard to debug on the Windows installer (@ejgallego, ejgallego/coq-lsp#557) - Add pointers to Windows installers (@ejgallego, ejgallego/coq-lsp#559) - Recognize `Goal` and `Definition $id : ... .` as proof starters (@ejgallego, ejgallego/coq-lsp#561, reported by @Zimmi48, fixes ejgallego/coq-lsp#548) - Provide basic notation information on hover. This is intended for people to build their own more refined notation feedback systems (@ejgallego, ejgallego/coq-lsp#562) - Hover request can now be extended by plugins (@ejgallego, ejgallego/coq-lsp#562) - Updated LSP and JS client libs, notably to vscode-languageclient 9 (@ejgallego, ejgallego/coq-lsp#565) - Implement a LIFO document scheduler, this is heavier in the background as more documents will be checked, but provides a few usability improvements (@ejgallego, ejgallego/coq-lsp#566, fixes ejgallego/coq-lsp#563, reported by Ali Caglayan) - New lexical qed detection error recovery rule; this makes a very large usability difference in practice when editing inside proofs. (@ejgallego, ejgallego/coq-lsp#567, fixes ejgallego/coq-lsp#33) - `coq-lsp` is now supported by the `coq-nix-toolbox` (@Zimmi48, @CohenCyril, ejgallego/coq-lsp#572, via coq-community/coq-nix-toolbox#164 ) - Support for `-rifrom` in `_CoqProject` and in command line (`--rifrom`). Thanks to Lasse Blaauwbroek for the report. (@ejgallego, ejgallego/coq-lsp#581, fixes ejgallego/coq-lsp#579) - Export Query Goals API in VSCode client; this way other extensions can implement their own commands that query Coq goals (@amblafont, @ejgallego, ejgallego/coq-lsp#576, closes ejgallego/coq-lsp#558) - New `pretac` field for preprocessing of goals with a tactic using speculative execution, this is experimental for now (@amblafont, @ejgallego, ejgallego/coq-lsp#573, helps with ejgallego/coq-lsp#558) - Implement `textDocument/selectionRange` request, that will return the range of the Coq sentence underlying the cursor. In VSCode, this is triggered by the "Expand Selection" command. The implementation is partial: we only take into account the first position, and we only return a single range (Coq sentence) without parents. (@ejgallego, ejgallego/coq-lsp#582) - Be more robust to mixed-separator windows paths in workspace detection (@ejgallego, ejgallego/coq-lsp#583, fixes ejgallego/coq-lsp#569) - Adjust printing breaks in error and message panels (@ejgallego, @Alizter, ejgallego/coq-lsp#586, fixes ejgallego/coq-lsp#457 , fixes ejgallego/coq-lsp#458 , fixes ejgallego/coq-lsp#571)
nberth
pushed a commit
to nberth/opam-repository
that referenced
this issue
Jun 18, 2024
CHANGES: ------------------------------- - Update VSCode client dependencies, should bring some performance improvements to goal pretty printing (@ejgallego, ejgallego/coq-lsp#530) - Update goal display colors for light mode so they are actually readable now. (@bhaktishh, ejgallego/coq-lsp#539, fixes ejgallego/coq-lsp#532) - Added link to Python coq-lsp client by Pedro Carrot and Nuno Saavedra (@Nfsaavedra, ejgallego/coq-lsp#536) - Properly concatenate warnings from _CoqProject (@ejgallego, reported by @mituharu, ejgallego/coq-lsp#541, fixes ejgallego/coq-lsp#540) - Fix broken `coq/saveVo` and `coq/getDocument` requests due to a parsing problem with extra fields in their requests (@ejgallego, ejgallego/coq-lsp#547, reported by @Zimmi48) - `fcc` now understands the `--coqlib`, `--coqcorelib`, `--ocamlpath`, `-Q` and `-R` arguments (@ejgallego, ejgallego/coq-lsp#555) - Describe findlib status in `Workspace.describe`, which is printed in the output windows (@ejgallego, ejgallego/coq-lsp#556) - `coq-lsp` plugin loader will now be strict in case of a plugin failure, the previous loose behavior was more convenient for the early releases, but it doesn't make sense now and made things pretty hard to debug on the Windows installer (@ejgallego, ejgallego/coq-lsp#557) - Add pointers to Windows installers (@ejgallego, ejgallego/coq-lsp#559) - Recognize `Goal` and `Definition $id : ... .` as proof starters (@ejgallego, ejgallego/coq-lsp#561, reported by @Zimmi48, fixes ejgallego/coq-lsp#548) - Provide basic notation information on hover. This is intended for people to build their own more refined notation feedback systems (@ejgallego, ejgallego/coq-lsp#562) - Hover request can now be extended by plugins (@ejgallego, ejgallego/coq-lsp#562) - Updated LSP and JS client libs, notably to vscode-languageclient 9 (@ejgallego, ejgallego/coq-lsp#565) - Implement a LIFO document scheduler, this is heavier in the background as more documents will be checked, but provides a few usability improvements (@ejgallego, ejgallego/coq-lsp#566, fixes ejgallego/coq-lsp#563, reported by Ali Caglayan) - New lexical qed detection error recovery rule; this makes a very large usability difference in practice when editing inside proofs. (@ejgallego, ejgallego/coq-lsp#567, fixes ejgallego/coq-lsp#33) - `coq-lsp` is now supported by the `coq-nix-toolbox` (@Zimmi48, @CohenCyril, ejgallego/coq-lsp#572, via coq-community/coq-nix-toolbox#164 ) - Support for `-rifrom` in `_CoqProject` and in command line (`--rifrom`). Thanks to Lasse Blaauwbroek for the report. (@ejgallego, ejgallego/coq-lsp#581, fixes ejgallego/coq-lsp#579) - Export Query Goals API in VSCode client; this way other extensions can implement their own commands that query Coq goals (@amblafont, @ejgallego, ejgallego/coq-lsp#576, closes ejgallego/coq-lsp#558) - New `pretac` field for preprocessing of goals with a tactic using speculative execution, this is experimental for now (@amblafont, @ejgallego, ejgallego/coq-lsp#573, helps with ejgallego/coq-lsp#558) - Implement `textDocument/selectionRange` request, that will return the range of the Coq sentence underlying the cursor. In VSCode, this is triggered by the "Expand Selection" command. The implementation is partial: we only take into account the first position, and we only return a single range (Coq sentence) without parents. (@ejgallego, ejgallego/coq-lsp#582) - Be more robust to mixed-separator windows paths in workspace detection (@ejgallego, ejgallego/coq-lsp#583, fixes ejgallego/coq-lsp#569) - Adjust printing breaks in error and message panels (@ejgallego, @Alizter, ejgallego/coq-lsp#586, fixes ejgallego/coq-lsp#457 , fixes ejgallego/coq-lsp#458 , fixes ejgallego/coq-lsp#571)
nberth
pushed a commit
to nberth/opam-repository
that referenced
this issue
Jun 18, 2024
CHANGES: ------------------------------- - Update VSCode client dependencies, should bring some performance improvements to goal pretty printing (@ejgallego, ejgallego/coq-lsp#530) - Update goal display colors for light mode so they are actually readable now. (@bhaktishh, ejgallego/coq-lsp#539, fixes ejgallego/coq-lsp#532) - Added link to Python coq-lsp client by Pedro Carrot and Nuno Saavedra (@Nfsaavedra, ejgallego/coq-lsp#536) - Properly concatenate warnings from _CoqProject (@ejgallego, reported by @mituharu, ejgallego/coq-lsp#541, fixes ejgallego/coq-lsp#540) - Fix broken `coq/saveVo` and `coq/getDocument` requests due to a parsing problem with extra fields in their requests (@ejgallego, ejgallego/coq-lsp#547, reported by @Zimmi48) - `fcc` now understands the `--coqlib`, `--coqcorelib`, `--ocamlpath`, `-Q` and `-R` arguments (@ejgallego, ejgallego/coq-lsp#555) - Describe findlib status in `Workspace.describe`, which is printed in the output windows (@ejgallego, ejgallego/coq-lsp#556) - `coq-lsp` plugin loader will now be strict in case of a plugin failure, the previous loose behavior was more convenient for the early releases, but it doesn't make sense now and made things pretty hard to debug on the Windows installer (@ejgallego, ejgallego/coq-lsp#557) - Add pointers to Windows installers (@ejgallego, ejgallego/coq-lsp#559) - Recognize `Goal` and `Definition $id : ... .` as proof starters (@ejgallego, ejgallego/coq-lsp#561, reported by @Zimmi48, fixes ejgallego/coq-lsp#548) - Provide basic notation information on hover. This is intended for people to build their own more refined notation feedback systems (@ejgallego, ejgallego/coq-lsp#562) - Hover request can now be extended by plugins (@ejgallego, ejgallego/coq-lsp#562) - Updated LSP and JS client libs, notably to vscode-languageclient 9 (@ejgallego, ejgallego/coq-lsp#565) - Implement a LIFO document scheduler, this is heavier in the background as more documents will be checked, but provides a few usability improvements (@ejgallego, ejgallego/coq-lsp#566, fixes ejgallego/coq-lsp#563, reported by Ali Caglayan) - New lexical qed detection error recovery rule; this makes a very large usability difference in practice when editing inside proofs. (@ejgallego, ejgallego/coq-lsp#567, fixes ejgallego/coq-lsp#33) - `coq-lsp` is now supported by the `coq-nix-toolbox` (@Zimmi48, @CohenCyril, ejgallego/coq-lsp#572, via coq-community/coq-nix-toolbox#164 ) - Support for `-rifrom` in `_CoqProject` and in command line (`--rifrom`). Thanks to Lasse Blaauwbroek for the report. (@ejgallego, ejgallego/coq-lsp#581, fixes ejgallego/coq-lsp#579) - Export Query Goals API in VSCode client; this way other extensions can implement their own commands that query Coq goals (@amblafont, @ejgallego, ejgallego/coq-lsp#576, closes ejgallego/coq-lsp#558) - New `pretac` field for preprocessing of goals with a tactic using speculative execution, this is experimental for now (@amblafont, @ejgallego, ejgallego/coq-lsp#573, helps with ejgallego/coq-lsp#558) - Implement `textDocument/selectionRange` request, that will return the range of the Coq sentence underlying the cursor. In VSCode, this is triggered by the "Expand Selection" command. The implementation is partial: we only take into account the first position, and we only return a single range (Coq sentence) without parents. (@ejgallego, ejgallego/coq-lsp#582) - Be more robust to mixed-separator windows paths in workspace detection (@ejgallego, ejgallego/coq-lsp#583, fixes ejgallego/coq-lsp#569) - Adjust printing breaks in error and message panels (@ejgallego, @Alizter, ejgallego/coq-lsp#586, fixes ejgallego/coq-lsp#457 , fixes ejgallego/coq-lsp#458 , fixes ejgallego/coq-lsp#571)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Describe the bug
If multiple warning display options are specified in the _CoqProject file, they are not respected.
To Reproduce
Steps to reproduce the behavior:
Print Options.and move the cursor to just before the period.Expected behavior
The output contains the line
Warnings: "-notation-overridden,+duplicate-clear,+non-primitive-record,+undeclared-scope,+deprecated-hint-without-locality"with a comma-separated string.Actual behavior
The corresponding line has no comma:
Warnings: "-notation-overridden+duplicate-clear+non-primitive-record+undeclared-scope+deprecated-hint-without-locality"Desktop (please complete the following information):
The text was updated successfully, but these errors were encountered: