Stream: coq-lsp

Topic: Misc errors in my first testing


view this post on Zulip Paolo Giarrusso (Apr 15 2023 at 13:13):

EDIT: I installed coq-lsp, and I'm running into a few issues. I see enough that I'm just collecting them into this thread.

  1. Missing serlib plugin: coq-elpi.elpi — is this warning a problem?
  2. We also build custom plugins, and it seems coq-lsp can't find them, neither from _CoqProject (even if it loads okay) nor if I rely on a pure dune setup (aka, after rm _CoqProject).

view this post on Zulip Paolo Giarrusso (Apr 15 2023 at 13:32):

  1. new: I tried Restart and got Restart cannot be used through the Load command, which is a first in my life since this code is Load-free...

view this post on Zulip Paolo Giarrusso (Apr 15 2023 at 13:40):

  1. warning settings from _CoqProject are ignored entirely, which makes my code very noisy

view this post on Zulip Paolo Giarrusso (Apr 15 2023 at 13:43):

issue 2. blocks me from trying this on most code from my work projects. All I _wanted_, tho, was to try this on _slow_ proofs to see how the interaction mode behaves, so I moved to my hobby project

view this post on Zulip Paolo Giarrusso (Apr 15 2023 at 15:07):

  1. There isn't a way to enable/disable this per-project. That's fine for me, but it does mean I will have to disable this globally — instead of enabling it for projects that work.

Generally, this is pretty interesting!

view this post on Zulip Ali Caglayan (Apr 17 2023 at 09:26):

  1. This warning is not a problem, it is just from quickly reusing the serapi plugin loading lib. AFAIK
  2. It's entirely possible that is a problem, please open a ticket.
  3. Restart is probably not supported atm, please open a ticket. (I suspect the load warning is from sharing a codepath)
  4. No special handling for this IIRC.
  5. You have workspace local settings in VSCode IIRC. There you can use the disabling feature in the config for each project you wish. The status bar button can also be clicked to enable disable quickly.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2023 at 14:17):

Thanks a lot for testing @Paolo Giarrusso Indeed what @Ali Caglayan says, let me add a couple of extra points:

  1. this warning is a dev-only warning, sorry for that, I will disable it in released versions; it means that for Elpi you get worse incrementatily as coq-lsp didn't install it's custom Ast processor.
  2. yes please open a bug, note that (funnily enough) we don't yet recognize dune files
  3. Restart is indeed not supported, the message is coming from Coq so this is why it mentions Load (as this codepath can be only triggered by Coq when using Load)
  4. def open an issue for this, the code to update is coq/workspace.ml:parse_args , that's an easy todo I think
  5. I think we should be able to solve 2 quickly once we get an example

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2023 at 14:18):

What do you need to enable / disable per-project? I'm not sure I understood

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2023 at 14:25):

Regarding large proofs, IMHO we need some further improvements in Coq to handle them in the way I would like.

As of today, due to the way Coq works, it is not possible to "read" information of a document from, let's say, a different thread without interrupting what Coq is computing. That's a really bad point for systems like coq-lsp as when the user requests info you either:

First problem can be alleviated by using a cache, however there are non trivial tradeoffs involved. Let's see how things go.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2023 at 14:25):

Moreover there is no connection between the incrementality of the proof / logic programming engine and the incrementality at the sentence level, this is for sure desired in many scenarios.

view this post on Zulip Paolo Giarrusso (Apr 18 2023 at 16:36):

What do you need to enable / disable per-project? I'm not sure I understood

s/project/workspace/g — but Ali answered that: Vscode lets one disable extensions for workspace

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2023 at 17:14):

Ah, you mean the extension itself: yes, it can be disabled per-workspace.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2023 at 17:14):

Happy to implement some other technique if folks have the need to tell coq-lsp "don't touch this"


Last updated: Mar 29 2024 at 15:02 UTC