coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Emilio Jesús Gallego Arias <e AT x80.org>
- To: Coq Club <coq-club AT inria.fr>
- Subject: [Coq-Club] [ANN] coq-lsp release 0.1.2
- Date: Sun, 08 Jan 2023 19:38:49 +0100
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Pass smtp.mailfrom=e AT x80.org; spf=Pass smtp.helo=postmaster AT x80.org
- Ironport-data: A9a23:675E/6mFfacUUdBzNTZMZCfo5gwBI0RdPkR7XQ2eYbSJt1+Wr1Gzt xJMXGDXOPyOMDP2LthxPNnkph8EvZ7QxocxHAY/pX83FVtH+JHPbTi7BhepbnnKdqUvb2o+s p5AMoGYRCwQZiWBzvt4GuG59RGQ7YnRGvymTres1hlZHWdMUD0mhQ9oh9k3i4tphcnRKw6Ws LsemeWGULOe82MyYzx8B56r8ks156yr4GNA5zTSWNgS1LPgvylNZH4gDfrpR5fIatE8NvK3Q e/F0Ia48gvxl/v6Io7Nfh7TKyXmc5aKVeS8oiI+t5uK3nCukhcPPpMTb5LwX6v4ZwKhxLidw P0V3XC5pJxA0qfkwIzxWDEAe81y0DEvFBYq7hFTvOTKp3AqfUcAzN1hAkM3FqgkwNpFX2hBx 9wcczcnMh2c0rfeLLKTEoGAh+wzfJGtO5kQ0p1i5WiJXbB8G86FGvqTo4YDhl/chegWdRraT 8cxeWo3KhPabHWjP39LVM5hxrz31xETdRVokFyOp5Ets1TI3VRtyZ2qLMfoddGjEJA9ckGw/ DidozWkUnn2Lue3wj2ct3mom+XnhjL+QItUFbui9/csjkf7+4AIIA1GDR28u/bRZlOCt8x3J EIW+wELkZIOxhKiQevdW0a/iiKJoUtJMzZPKNHW+D1h24KNvVnCXjVUFmcfADA1nJJsHmRyi zdli/u1VGAw4dV5XFrHrt+pQSWO1T89C0tqicUsZA4e/9T5rIg25v4kZo86SPPdYjHdPzbq3 zDCjC86g7wVgaY2O0SHEbPv2m3ESmDhFFJd2+kudjvNA8MQTNfNi3aUwVba9+1cC42SU0OMu nMJ8+DHsr9VVMjTznbXEbRTdF1M2xpjGGKC6bKIN8Z8nwlBB1b6J+i8HRkkeRk3Y55YEdMXS BOC6V0BjHOsAJdaRfUtON7gVpRCIVnIGdXqV+zdapJJaZV4cme6ENJGNSatMqGEuBZErJzTz r/CL57yVS1FV/45pNd0Ls9EuYIWKukF7Tu7bfjGI96PiNJyvVbFFelXA0jEde0j8qKPrSPc9 tsVZYPAyAxSXKe6KmPb+JIaZwJCZ3UqJ4HEm+oOfM66Iy1iBD4ADd3VyugfYIBLpfleudrJ2 XCfYXVm7mTDq0fJEii0T0xySajOWM9/pE0rPCZ3MleP3WMiULmV76weVsUWe7Z70cc+0/VxR PghUOeDC8RpVT7o1Wk8b578jYo6bzWtp1uEEBSEaQgFXaxLZlL26P69WSW37wgILC68lfVmk o2azgmBHKYyHVVzPvjZeNeE7g2Xv0FEvMlQQkGRAN1YWHu0wbhQMyar08MGeZAdGy7imAmf+ R2dWyoDhO/3pIQwztnFqIaEo6qtEMp8BkBqJHba35nnKRjl+nef/qEYXNaqZTz9UEbGyJemb 8hRzND+N6QJp0YVkoxeF70w87kyyeGyrJBnzyNlPk7xUXKVNp1aLEKr5/J/7p92+ucBuC+de F6+xd1BCLDYZOLnCAEwISQmXMSi1NYVuGX1wd0oKh7Y4g5247u1fkFANDaciCFmDeVUMaF05 cwDqcIp+wiEpR5yCem/jwdQ7HWqEnwMd44Fp6MqKtbnpSRzw24TfKGGLDH95a++TullM24oE 2eyv7XDjbEN/XjyWSM/OlaV1NUMmKlUng5ByWIDAFG7mtDloPsT9z8J+BQVSjVl9Dl249hRC ENKaXIsfb6v+g12jvdtR2qvQgFNJCOI83zLlmcmqjfrcFmKZEfscksNYf2A7WIIwVJ6JzJ7x oyV+EzhcDTtffzy4BcMZF5Ym6TdauJ1pyL/m5GBPsWaHpMFTyLvrY2waEEp9Rb2I8MDq3fWh Ott/etcZrLfMH8BkbwaEKif76wbEzqfFVxBQNZg3aIHJn7dczeMwgqzK1i9V8dOBv7S+2q6N pBeHd1OXBGAyyq+lDAXKqoSKbtSnvRyxt49Vp70BGwB6Z2zkyFItc/Oyy3Am2MbedVivsIjI If3dTjZMGixh2NRqlDdvvt/JWu0TtkVVjLShNnv3r0yKKsCl+VwfWUZ8Li+5SyVOTQ62SOkh lrIYquOwtFyzYhpoZDXLZxCIAeKeOPDDLHCtEj5ttlVdtrAPPvfrw5f+BGtIw1SOqBXQNht0 6iEtNnsxk7eobIqSCbjloKcE7VSr9CHNAaN3hkb8FEB9cdDZCPt3/fH03DocdpOitw1CgyPW V6jcMXpHTIKc441+ZGXQ3E2/9Uh52Dffve44ySnoJxgzzADhBffIorPGWDBNAlmm+xhB3E6I h+k47Cp/N8wQEGgwvMbL6kOPqKU62MPlUfrmxMdeNVY4qSVbou+h4bf
- Ironport-hdrordr: A9a23:YovI1a7/KkrxcCtRqgPXwPzXdLJyesId70hD6qkXc20yTiX4rb HIoB1/73TJYVkqKRIdcLy7VZVoIkmskaJdxYEQOPOMWgzivnW1NcVe6+LZowEIeReOlNK1BZ 0PT0EWMrSZZ2SS5vyU3ODXKbodKZW8gcWVbSq19RZQcT0=
- Ironport-phdr: A9a23:JK8DTxaSfQ1NRRksBkb3YML/LTH524qcDmcuAnoPtbtCf+yZ8oj4O wSHvLMx1gKPDdmQsqsaw8Pt8IneGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpV O5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxtIiTanYr5/I xq6oRjMusQXnIBvNrs/xhzVr3RHfOhb2XlmLk+JkRbm4cew8p9j8yBOtP8k6sVNT6b0cbkmQ LJBFDgpPHw768PttRnYUAuA/WAcXXkMkhpJGAfK8hf3VYrsvyTgt+p93C6aPdDqTb0xRD+v4 btnRAPuhSwaLDMy7n3ZhdJsg6JauBKhpgJww4jIYIGOKfFyerrRcc4GSWZdW8pcUTFKDIGhY IsVF+cPPfhWoZT6p1UArhWxCwajC//gxDJTmn/2xLc33/g9HQzc3gEtGc8FvnTOrNXyMacfS e+7zKzJzTXHbvNW3ir25ozWfRA6u+mMRq97f8vLxkkrEwPKkFqQqYv4ND6JzOQNsnKU7/F9X u+olWEqsA5wrzuzyss2jYnJnI0Vx0nC+C5kz4k7Oce2R1RnYd64DpRQrSeaOpNrT848TW9mt zs2x70ItJC7YSUG1JYqyh/QZfGbb4WF7RHuWPiMLTp8gH9oZbOyiRmx/EagyeDyWdS43VdEo CZYlNTHq34D1xvW6sedS/t9+F+s2TmO1wDP6uFEPFs7mbDHJJ4mx748jpQTvl7aHiPsnUX5k bead0Q5+uis6uTneqnppp+GOI9okA3xLqMumsm5DO8lMQYOR3CW9fm/2bDg50H1XqtGg/wsn qXEsp3WON4XqrO3DgNLyoou6RSyAy243NgEknQLNk9JdA6FgoTzJl3DJu3zA+2/g1Stizdrx /HGPrvuApvONnjNiKnufapz6k5b0gozzshS649XB7wCOv7/RFH9ud3CAhMkMQG43vzrBMhz2 48AX2+EH7WXP7nIsVCS4+IiO+mMa5ERuDb6M/Uk6P3jgWMjlV8aZ6mp0oMbaHG+Hvt4P0WUe Wfgj9QCHGsQoAYyUu3nhEefXTNRenq+Rb8w6z8lBI6+CIfMXIGtgLiP3CehGZ1WY3hLBU6XH HbndIiIR+0AaCWIIs9uijAEU6OuRJc71R6yrA/616ZnLu3M9yEFrZ7jzsR65/XPlREu8jx5F 9iS02aUT21tgmwIQyI207tkrExmylaD1LB4jOZCGdxS4fNJSAY6OoTGw+x0EdChEj7GK/yOU R6NRsisSWU6Sct0yNsTaW58Hc+jh1bNxXz5LaUSkummAZ0w86WU/XXqtd015H/C0KQuiBEPW MpGLiXyi4Zvp1CVAJTGxRbK3522fLgRiXaevFyIynCD6QQBCFYYucTtWHkeYhCTttHl/gbZS KfoD707MwxHwMrEK61Qa9Svg08VDOz7NoH4ZGS803y1GQ7O3qmFOYfCazVFmiLHBxtMiBgdq E6PLhN2HSK9uyTbBT1qG0joZhbh2fku8DW8VEBnhxqSYRhZ3qGusgUQmeTaS/4X2eccvzw9r jxvAFun98KGU5yHvQUJkLx0R9Q77R8H0GvYs1c4JZm8N+V5gUZYdQ1rvkTo3hExC4NakMFso ml4hAx1YbmV1l9MbVb6ldj5J6HXJ2/u/Ruud7+e21fQ18yT87sO7/JwokvqvQWgHE4vu3t91 Nwd33yZ75TMRA0cGZ/ZQhZvsR9gqPC/AGF15o/Z02FtLbjhqiXLiJoiAOoozArlfs8KafPUU lWoTYtDWJHocbdwyD3LJloeMetf9bA5JZajfvqCg+uwOfp42SmhlSJB6Zx81USF82x9TPTJ1 tAL2aL9vEPPWjHigVOmqs2yl5pDYGRYE0KvmXCiA5ReLP46bcMQBGGiLtfijNhWl861HXlC+ xTwYjFOkN/sch2UYVvn2ARW3klCun2rlxyzyDlsmi0opK6StMDX69zrbwFPemtCRW05yEzpP ZDxlNcCGk6hcwkukhKho0f83alS4qplfSHfRkJBfi6+KG8HMOP4u5KSM5YJ74kn+SlaS+WzZ 1mGR6W1+ktKlXm5QS0Hm2l9Lmrw8pzi1wR3kmecMGp+oDLCdMd8yA2egb6UDf9d0zwaRTVp3 DzeB1yyJd6srp2fk5bOtPz7Vnr0D80DN3Oxk8XZ63L9vDYwUnjd17ipl9bqEBY3y3r+3thuD mDTqQrkJ5Lsz+K8OP5meU9hABn97dB7E8dwiNhV5tlY1H4Ei5GS5XdCn330NIAR1IruPCJLQ iQEiY2d8E3+1UtvI2jcjY/RRiXFhMx7aJPpBwFekjJ45MdMBqCO6bVCliYguVu0ozXaZv1ll yscw/8juzYKxvsEsw03wmCBE6gfSANGaDf0mU3CvLXc5O1HIXyier+q2A9ikMC9Wfuc9xpEV i+xf4dqFGdo8t83Z1vI1DebBpjMQNDLdppTsxSVl0yFlO1JMNcqkeJMgyN7OGX7tHljyughj BUo04vo9ISALmxs+uq+DHs6fnXtYNgP/zj2katEttbGh8aoBJopFjgQXZTuRO6lC3pL5aShb VzQVmRj8zHCQuCXFBTX8Ep8qnPTD52nUhPfbGIUy9lvXljVJUBShhwVQCRvnpM9EVPiz8jgf UFlozEJsweo+l0WkLwubkamFD6E/lTNCH98UpWUIRtI4xsX4k7UNZfb9edvB2RD+YXnqgWRK 2udbgAODGcTW0XCCUqwW9vmrdTG7eWcAfKzavXUZrDb4+F2R6fQg5W13cE1tybJLciJMnR4W rcj3VFfWHliB8nDsyVfE2oQjS2HPKv57F+svyZwqM646vHiXgnisJCOB7VlOtJq4xmqgK2HO r3YlGNjJD1fzJ9J2W7Qxe1VwgsJky83PWrIc/xIpWvXQanXgKMSExMLd3Y5Kp5T96xllgxdc ceTks/vnulxivp/Y7+kfUyxwoeuf8NYeglV23vXVB7NM66Jd2SjKyTfcfPkD7pKg7cM3yA=
- Ironport-sdr: 63bb0dd4_f9OiUJhqXWhS3U0V5kt4RDIH/6clRZ8z3kNNvOUsDYgrELv Bj29/Dn+Rs63ckRIsutCwAD0gNWVqhE/5t6T1bA==
- Organization: X80 Heavy Industries
Dear all,
we are happy to announce the release of coq-lsp 0.1.2, a new language
Server and VSCode extension for the Coq interactive proof assistant.
`coq-lsp` aims to provide a modern and streamlined proof-editing
experience, supporting incremental checking, markdown documents, and an
error recovery strategy friendly to step wise development of proof
documents.
The 0.1.2 release has been significantly improved since the 0.1.0
preview release, we encourage Visual Studio Code users to try it!
(make sure that the client and server version coincide, and see below
for known issues)
See the `coq-lsp` F.A.Q. [1] for some often asked questions.
Don't hesitate to stop by our Zulip [2] channel to chat, provide
feedback, or report bugs.
`coq-lsp` is developed in an open, collaborative way, if you are
interested in helping, we are really looking forward to it. There are
many interesting projects that can be done with `coq-lsp` as a base.
The first `coq-lsp` developers and user online meeting will take place
Monday January 9th, at 5pm Paris time, see [3] for details.
The main known issue is that coq-lsp won't properly handle yet proving
with multiple buffers, this is due to problems in Coq upstream, Coq
developers and in particular Gaëtan Gilbert are working in a fix.
If you find this issue, simply close all other .v files and restart the
server.
The full changelog for this release is:
# coq-lsp 0.1.2: Message
------------------------
- 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 of `coq-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. The `show_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)
# coq-lsp 0.1.1: Location
-------------------------
- Don't crash if the log file can't be created (@ejgallego, #87)
- Use LSP functions for client-side logging (@ejgallego, #87)
- Log `_CoqProject` detection settings to client window (@ejgallego, #88)
- Use plugin include paths from `_CoqProject` (@ejgallego, #88)
- Support OCaml >= 4.12 (@ejgallego, #93)
- Optimize the number of diagnostics sent in eager mode (@ejgallego, #104)
- Improved syntax highlighting on VSCode client (@artagnon, #105)
- Resume document checking from the point it was interrupted
(@ejgallego, #95, #99)
- Don't convert Coq "Info" messages such as "Foo is defined" to
feedback by default; users willing to see them can set the
corresponding option (@ejgallego, #113)
- Send `$/coq/fileProgress` progress notifications from server,
similarly to what Lean does; display them in Code's right gutter
(@ejgallego, #106, fixes #54)
- Show goals on click by default, allow users to configure the
behavior to follow cursor in different ways (@ejgallego, #116,
fixes #89)
- Show file position in goal buffer, use collapsible elements for
goal list (@ejgallego, #115, fixes #109)
- Resume checking from common prefix on document update (@ejgallego,
#111, fixes #110)
- Only serve goals, hover, and symbols requests when the document
has been sufficiently processed (@ejgallego, #120, fixes #100)
Kind regards,
The coq-lsp team
[1] https://github.com/ejgallego/coq-lsp/blob/main/etc/FAQ.md
[2] https://coq.zulipchat.com/#narrow/stream/329642-coq-lsp
[3] https://github.com/ejgallego/coq-lsp/wiki/Coq-Lsp-Calls
Errata for the 0.1.0 release mail: we forgot Vincent Laporte in the
list of contributors, who contributed the first version of the VSCode
client. Thanks Vincent and sorry!
- [Coq-Club] [ANN] coq-lsp release 0.1.2, Emilio Jesús Gallego Arias, 01/08/2023
- Re: [Coq-Club] [ANN] coq-lsp release 0.1.2, Emilio Jesús Gallego Arias, 01/08/2023
Archive powered by MHonArc 2.6.19+.