CHANGES:
- Send an error to the client if the client and server versions don't
match (@ejgallego, #126) - Parse options -noinit, -indices-matter, and -impredicative-set from
_CoqProject
(@artagnon, @ejgallego, #140, #150) - Log file
log-lsp.txt
has been removed in favor ofcoq-lsp.trace.server
(@artagnon, @ejgallego, #130, #148) - Added --bt flag to print a backtrace on error (@Alizter, #147)
- A detailed view of Coq errors is now displayed in the info panel
(@ejgallego, #128) - Coq "Notice" messages, such as the ones generated by
About
or
Search
are not shown anymore as diagnostics. Instead, they will
be shown on the side panel when clicking on the corresponding
command. Theshow_notices_as_diagnostics
option allows to restore
old behavior (@ejgallego, #128, fixes #125) - Print some more info about Coq workspace configuration (@ejgallego, #151)
- Admit failed
Qed
by default; allow users to configure it
(@ejgallego, #118, fixes #90)