Visual Studio Code Extension and Language Server Protocol for Coq
LGPL-2.1 License
Bot releases are hidden (Show)
CHANGES:
show_loc_info_on_hover
that will display parsing debug.mv
vscode-languageclient
9 which imposes this. (@ejgallego, #599,proof/goals
request: new mode
parameter, to specify goalspretac
to command
, as toastdump
plugin to dump AST of files into JSON andgoal_after_tactic
to true
(@Alizter,Defined
and Admitted
in lex recoverycheck_only_on_request
which will delay--no_vo
for fcc
, which will skip the .vo
saving.vo
saving is now an fcc
plugins, but for now, it ismemprof-limits
on OCaml 4.x (@ejgallego, #660)memprof-limits
coq-lsp.plugin.goaldump
plugin, as an example on how to dumpCoq LSP: Toggle heatmap
selectionRange
LSP callcoq-lsp.sentenceNext
/ coq-lsp.sentencePrevious
Alt + N
/ Alt + P
keybindingsextra
field to data
, so we now conform to thesend_diags_extra_data
coq-lsp.pp_type
VSCode client option now takes effectvsls://
), inInjectRequire
plugin API for plugins to be able to instrument--max_errors=n
option to fcc
, this way users can set--max_errors=0
to imitate coqc
behavior (@ejgallego, #680)fcc
exit status when checking terminates with fatal errorsmain
branch (@ejgallego, #683,--int_backend={Coq,Mp}
command line parameter to select thepackage-lock.json
for latest bugfixes (@ejgallego, #687)prettier
(@Alizter @ejgallego, #684 #688)coq/perfData
call (@ejgallego @Alizter, #689)coq/perfData
(@ejgallego, #689)coq/perfData
(@ejgallego, #717)coq-lsp.document
VSCode command will now display the returnedworkspace/didChangeConfiguration
(@ejgallego, #702)petanque
API to interact directly with Coq's proofpetanque
JSON-RPC pet.exe
, which can be used à la SerAPIpet-server.exe
TCP server for keep-alive sessions (@gbdrt,Coq LSP: Toggle heatmap
coq/viewRange
notification, from client tosentenceNext/sentencePrevious
(@ejgallego, #718)Goals
panel focus back if it has lost it (in case offcc
: new option --diags_level
to control whether Coq's notice.lv / .v.tex
TeX files with embedded Coq coderun_tac
, so wegoals
round-trip for each tactic (@gbdrt, @ejgallego,LanguageStatusItem
Published by ejgallego 5 months ago
CHANGES:
show_loc_info_on_hover
that will display parsing debug.mv
vscode-languageclient
9 which imposes this. (@ejgallego, #599,proof/goals
request: new mode
parameter, to specify goalspretac
to command
, as toastdump
plugin to dump AST of files into JSON andgoal_after_tactic
to true
(@Alizter,Defined
and Admitted
in lex recoverycheck_only_on_request
which will delay--no_vo
for fcc
, which will skip the .vo
saving.vo
saving is now an fcc
plugins, but for now, it ismemprof-limits
on OCaml 4.x (@ejgallego, #660)memprof-limits
coq-lsp.plugin.goaldump
plugin, as an example on how to dumpCoq LSP: Toggle heatmap
selectionRange
LSP callcoq-lsp.sentenceNext
/ coq-lsp.sentencePrevious
Alt + N
/ Alt + P
keybindingsextra
field to data
, so we now conform to thesend_diags_extra_data
coq-lsp.pp_type
VSCode client option now takes effectvsls://
), inInjectRequire
plugin API for plugins to be able to instrument--max_errors=n
option to fcc
, this way users can set--max_errors=0
to imitate coqc
behavior (@ejgallego, #680)fcc
exit status when checking terminates with fatal errorsmain
branch (@ejgallego, #683,--int_backend={Coq,Mp}
command line parameter to select thepackage-lock.json
for latest bugfixes (@ejgallego, #687)prettier
(@Alizter @ejgallego, #684 #688)coq/perfData
call (@ejgallego @Alizter, #689)coq/perfData
(@ejgallego, #689)coq/perfData
(@ejgallego, #717)coq-lsp.document
VSCode command will now display the returnedworkspace/didChangeConfiguration
(@ejgallego, #702)petanque
API to interact directly with Coq's proofpetanque
JSON-RPC pet.exe
, which can be used à la SerAPIpet-server.exe
TCP server for keep-alive sessions (@gbdrt,Coq LSP: Toggle heatmap
coq/viewRange
notification, from client tosentenceNext/sentencePrevious
(@ejgallego, #718)Goals
panel focus back if it has lost it (in case offcc
: new option --diags_level
to control whether Coq's notice.lv / .v.tex
TeX files with embedded Coq coderun_tac
, so wegoals
round-trip for each tactic (@gbdrt, @ejgallego,LanguageStatusItem
Published by ejgallego 5 months ago
CHANGES:
show_loc_info_on_hover
that will display parsing debug.mv
vscode-languageclient
9 which imposes this. (@ejgallego, #599,proof/goals
request: new mode
parameter, to specify goalspretac
to command
, as toastdump
plugin to dump AST of files into JSON andgoal_after_tactic
to true
(@Alizter,Defined
and Admitted
in lex recoverycheck_only_on_request
which will delay--no_vo
for fcc
, which will skip the .vo
saving.vo
saving is now an fcc
plugins, but for now, it ismemprof-limits
on OCaml 4.x (@ejgallego, #660)memprof-limits
coq-lsp.plugin.goaldump
plugin, as an example on how to dumpCoq LSP: Toggle heatmap
selectionRange
LSP callcoq-lsp.sentenceNext
/ coq-lsp.sentencePrevious
Alt + N
/ Alt + P
keybindingsextra
field to data
, so we now conform to thesend_diags_extra_data
coq-lsp.pp_type
VSCode client option now takes effectvsls://
), inInjectRequire
plugin API for plugins to be able to instrument--max_errors=n
option to fcc
, this way users can set--max_errors=0
to imitate coqc
behavior (@ejgallego, #680)fcc
exit status when checking terminates with fatal errorsmain
branch (@ejgallego, #683,--int_backend={Coq,Mp}
command line parameter to select thepackage-lock.json
for latest bugfixes (@ejgallego, #687)prettier
(@Alizter @ejgallego, #684 #688)coq/perfData
call (@ejgallego @Alizter, #689)coq/perfData
(@ejgallego, #689)coq/perfData
(@ejgallego, #717)coq-lsp.document
VSCode command will now display the returnedworkspace/didChangeConfiguration
(@ejgallego, #702)petanque
API to interact directly with Coq's proofpetanque
JSON-RPC pet.exe
, which can be used à la SerAPIpet-server.exe
TCP server for keep-alive sessions (@gbdrt,Coq LSP: Toggle heatmap
coq/viewRange
notification, from client tosentenceNext/sentencePrevious
(@ejgallego, #718)Goals
panel focus back if it has lost it (in case offcc
: new option --diags_level
to control whether Coq's notice.lv / .v.tex
TeX files with embedded Coq coderun_tac
, so wegoals
round-trip for each tactic (@gbdrt, @ejgallego,LanguageStatusItem
Published by ejgallego 9 months ago
CHANGES:
coq/saveVo
and coq/getDocument
requests due to afcc
now understands the --coqlib
, --coqcorelib
,--ocamlpath
, -Q
and -R
arguments (@ejgallego, #555)Workspace.describe
, which is printedcoq-lsp
plugin loader will now be strict in case of a pluginGoal
and Definition $id : ... .
as proof starterscoq-lsp
is now supported by the coq-nix-toolbox
(@Zimmi48,-rifrom
in _CoqProject
and in command line--rifrom
). Thanks to Lasse Blaauwbroek for the report.pretac
field for preprocessing of goals with a tactic usingtextDocument/selectionRange
request, that will returnPublished by ejgallego 12 months ago
CHANGES:
coq/saveVo
and coq/getDocument
requests due to afcc
now understands the --coqlib
, --coqcorelib
,--ocamlpath
, -Q
and -R
arguments (@ejgallego, #555)Workspace.describe
, which is printedcoq-lsp
plugin loader will now be strict in case of a pluginGoal
and Definition $id : ... .
as proof starterscoq-lsp
is now supported by the coq-nix-toolbox
(@Zimmi48,-rifrom
in _CoqProject
and in command line--rifrom
). Thanks to Lasse Blaauwbroek for the report.pretac
field for preprocessing of goals with a tactic usingtextDocument/selectionRange
request, that will returnPublished by ejgallego 12 months ago
CHANGES:
coq/saveVo
and coq/getDocument
requests due to afcc
now understands the --coqlib
, --coqcorelib
,--ocamlpath
, -Q
and -R
arguments (@ejgallego, #555)Workspace.describe
, which is printedcoq-lsp
plugin loader will now be strict in case of a pluginGoal
and Definition $id : ... .
as proof starterscoq-lsp
is now supported by the coq-nix-toolbox
(@Zimmi48,-rifrom
in _CoqProject
and in command line--rifrom
). Thanks to Lasse Blaauwbroek for the report.pretac
field for preprocessing of goals with a tactic usingtextDocument/selectionRange
request, that will returnPublished by ejgallego 12 months ago
CHANGES:
coq/saveVo
and coq/getDocument
requests due to afcc
now understands the --coqlib
, --coqcorelib
,--ocamlpath
, -Q
and -R
arguments (@ejgallego, #555)Workspace.describe
, which is printedcoq-lsp
plugin loader will now be strict in case of a pluginGoal
and Definition $id : ... .
as proof starterscoq-lsp
is now supported by the coq-nix-toolbox
(@Zimmi48,-rifrom
in _CoqProject
and in command line--rifrom
). Thanks to Lasse Blaauwbroek for the report.pretac
field for preprocessing of goals with a tactic usingtextDocument/selectionRange
request, that will returnPublished by ejgallego about 1 year ago
CHANGES:
fcc
. fcc
allows to access mostcoq-lsp
without the need for a command line client,Notation
strings (@ejgallego, #422)null
, as per LSP spec,rootPath
is relative (#465, @ejgallego, report by Alexproof/goals
request now takes an optional formatting parameter--idle-delay=$secs
that controls how0.1
, using more aggressive0.01
can decrease latency of requests by ~4x_CoqProject
files are now applied (@ejgallego,coq-lsp
(@ejgallego, #511)send_perf_data
send_diags
, verbosity
Published by ejgallego over 1 year ago
CHANGES:
fcc
. fcc
allows to access mostcoq-lsp
without the need for a command line client,Notation
strings (@ejgallego, #422)null
, as per LSP spec,rootPath
is relative (#465, @ejgallego, report by Alexproof/goals
request now takes an optional formatting parameter--idle-delay=$secs
that controls how0.1
, using more aggressive0.01
can decrease latency of requests by ~4x_CoqProject
files are now applied (@ejgallego,coq-lsp
(@ejgallego, #511)send_perf_data
send_diags
, verbosity
Published by ejgallego over 1 year ago
CHANGES:
fcc
. fcc
allows to access mostcoq-lsp
without the need for a command line client,Notation
strings (@ejgallego, #422)null
, as per LSP spec,rootPath
is relative (#465, @ejgallego, report by Alexproof/goals
request now takes an optional formatting parameter--idle-delay=$secs
that controls how0.1
, using more aggressive0.01
can decrease latency of requests by ~4x_CoqProject
files are now applied (@ejgallego,coq-lsp
(@ejgallego, #511)send_perf_data
send_diags
, verbosity
Published by ejgallego over 1 year ago
CHANGES:
coq/getDocument
to get serialized full document_CoqProject
files in differentexit
LSP notificationcoq-lsp.ok_diagnostics
setting (@artagnon, #129)vscode-languageclient
to 8.1.0 (@ejgallego, @Alizter,COQLIB
and COQCORELIB
environment variables, added--coqcorelib
command line argument (@ejgallego, #403)ocamlpath
from the command line (@ejgallego, #408)coq-lsp.stats_on_hover_option
to re-enable it (@ejgallego, #412,coq-lsp
can now save .vo
files for files opened in thecoq/saveVo
request (@ejgallego, #417, fixes #339)Published by ejgallego over 1 year ago
CHANGES:
coq/getDocument
to get serialized full document_CoqProject
files in differentexit
LSP notificationcoq-lsp.ok_diagnostics
setting (@artagnon, #129)vscode-languageclient
to 8.1.0 (@ejgallego, @Alizter,COQLIB
and COQCORELIB
environment variables, added--coqcorelib
command line argument (@ejgallego, #403)ocamlpath
from the command line (@ejgallego, #408)coq-lsp.stats_on_hover_option
to re-enable it (@ejgallego, #412,coq-lsp
can now save .vo
files for files opened in thecoq/saveVo
request (@ejgallego, #417, fixes #339)Published by ejgallego over 1 year ago
CHANGES:
COQPATH
and OCAMLPATH
(@ejgallego, #364)Published by ejgallego over 1 year ago
CHANGES:
$/coq/fileProgress
offset
fieldcoq-lsp
incorrectly required the optional rootPath
rootUri
if presentcoq-lsp
will now reject opening multiple files when thedocumentSymbol
return type for newer DocumentSymbol[]
Published by ejgallego over 1 year ago
CHANGES:
--std
argument to the coq-lsp
binary has beenGoalAnswer
s now include the proof "stack" and better hypothesisGoalAnswer
version_CoqProject
, -impredicative-set
is now parsed correctlydebug
option in the client / protocol that will enable Coq's backtraces_CoqProject
file is now detected using LSP client rootPath
\
to trigger Unicode completion by the server. ThisPublished by ejgallego almost 2 years ago
CHANGES:
coq-lsp
now follows the LSP specification regardingcoq-lsp
will now warn the user when two files have been openeddocumentSymbols
will now be postponed until the document isPublished by ejgallego almost 2 years ago
CHANGES:
_CoqProject
(@artagnon, @ejgallego, #140, #150)log-lsp.txt
has been removed in favor of coq-lsp.trace.server
About
orSearch
are not shown anymore as diagnostics. Instead, they willshow_notices_as_diagnostics
option allows to restoreQed
by default; allow users to configure itPublished by ejgallego almost 2 years ago
CHANGES:
_CoqProject
detection settings to client window (@ejgallego, #88)_CoqProject
(@ejgallego, #88)$/coq/fileProgress
progress notifications from server,Published by ejgallego almost 2 years ago
CHANGES: