Stream: coq-lsp

Topic: I see nothing

view this post on Zulip Huỳnh Trần Khanh (Jan 16 2023 at 04:33):

probably hard to debug as I have nothing except this screenshot. there is absolutely nothing on the screen, even when I hit Alt+Enter. what could be the issue here nothing-in-infoview.png

ok, sorry, I'm working on a monster proof again

view this post on Zulip Ramkumar Ramachandra (Jan 16 2023 at 10:14):

@Huỳnh Trần Khanh Could you open the debug console, and paste the output here?

view this post on Zulip Emilio Jesús Gallego Arias (Jan 16 2023 at 14:26):

@Huỳnh Trần Khanh in the output window below, there is an output buffer called Coq LSP Server Events, but it seems to me that the problem can likely be that you are on different client / server versions

view this post on Zulip Emilio Jesús Gallego Arias (Jan 16 2023 at 14:26):

What is the version of the client, and what does coq-lsp --version say?

view this post on Zulip Emilio Jesús Gallego Arias (Jan 16 2023 at 14:26):

We need to find a better story for compat, hopefully in 0.2 series

view this post on Zulip Emilio Jesús Gallego Arias (Jan 16 2023 at 14:27):

I love monster proofs hahaha

view this post on Zulip Emilio Jesús Gallego Arias (Jan 16 2023 at 14:27):

@Ramkumar Ramachandra something we are not doing superb is actually giving a good error answer in the infoview goal

view this post on Zulip Emilio Jesús Gallego Arias (Jan 16 2023 at 14:28):

So in @Huỳnh Trần Khanh case, likely the client was ahead of the server, so the infoview got a message that couldn't be rendered, in this case we should be able to do some error handling

view this post on Zulip Emilio Jesús Gallego Arias (Jan 16 2023 at 14:28):

and show something more informative in the info view

view this post on Zulip Huỳnh Trần Khanh (Jan 17 2023 at 06:33):

coq-lsp --version: 0.01
Logs: https://pastebin.com/nKcNRSCZ, https://pastebin.com/36tAYNLU

view this post on Zulip Huỳnh Trần Khanh (Jan 17 2023 at 06:36):

errors.png

view this post on Zulip Emilio Jesús Gallego Arias (Jan 17 2023 at 10:29):

Hi @Huỳnh Trần Khanh , def the problem is that you need the coq-lsp server to be at 0.1.3

view this post on Zulip Emilio Jesús Gallego Arias (Jan 17 2023 at 10:29):

goals protocol is not compatible; I've improved the compatibility history a lot, now users should get a proper error message if there is a problem with the versioning, sorry for that

Last updated: Apr 20 2024 at 06:02 UTC