Stream: coq-lsp

Topic: Reusing ocaml-lsp stuff


view this post on Zulip Emilio Jesús Gallego Arias (Jul 01 2022 at 10:37):

Hi @Rudi Grinberg , I was discussing a bit with @Ali Caglayan about the following:

We are aware of lev, etc... Do you think the approach you are using in ocaml-lsp to manage merlin can work for our use case? Thanks!

view this post on Zulip Rudi Grinberg (Jul 01 2022 at 13:52):

Note that I run merlin in a separate thread - not a process. This saves me some latency although I doubt it’s essential

view this post on Zulip Rudi Grinberg (Jul 01 2022 at 13:53):

I do manage the ocamlformat processes in a similar way though and it seems to work fine

view this post on Zulip Rudi Grinberg (Jul 01 2022 at 13:55):

The cancellation scheme you describe seems sensible to me

view this post on Zulip Emilio Jesús Gallego Arias (Jul 01 2022 at 14:06):

Ah! Indeed that saves some latency, I was confused indeed.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 01 2022 at 14:06):

So if merlin hangs, the whole ocaml-lsp server hangs?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 01 2022 at 14:07):

Yes I saw ocamlformat was doing differently, I'll have a look thanks

view this post on Zulip Emilio Jesús Gallego Arias (Jul 01 2022 at 14:07):

@Ali Caglayan told me that lev should works better for us than lwt, right?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 01 2022 at 14:07):

but do you have a lev release on opam or should we just vendor it?

view this post on Zulip Rudi Grinberg (Jul 01 2022 at 14:11):

If merlin hangs, only the thread dedicated to merlin hangs.

view this post on Zulip Rudi Grinberg (Jul 01 2022 at 14:11):

But merlin never hangs, just serves some requests slowly

view this post on Zulip Rudi Grinberg (Jul 01 2022 at 14:12):

However the lsp server remains responsive throughout

view this post on Zulip Rudi Grinberg (Jul 01 2022 at 14:13):

but do you have a lev release on opam or should we just vendor it?

Whatever you prefer. I never published it since it was never needed for me.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 01 2022 at 14:13):

Rudi Grinberg said:

If merlin hangs, only the thread dedicated to merlin hangs.

Yup, but how does merlin yield control back to the server given that can't multi-thread

view this post on Zulip Emilio Jesús Gallego Arias (Jul 01 2022 at 14:13):

?

view this post on Zulip Rudi Grinberg (Jul 01 2022 at 14:14):

Ali Caglayan told me that lev should works better for us than lwt, right?

It would mean you would be able to reuse much more of my lsp server. But It’s indeed also better than Lwt in a few other ways as well.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 01 2022 at 14:14):

Yeah I had a look and indeed looks pretty nice I think, tho I'm not an expert

view this post on Zulip Rudi Grinberg (Jul 01 2022 at 14:15):

Merlin does not need to yield control. It runs in a posix thread so the operating system tries to schedule the lsp and merlin threads fairly.

view this post on Zulip Rudi Grinberg (Jul 01 2022 at 14:16):

In theory, one thread can starve the other by having some infinite loop that never allocates. But this never happens in practice

view this post on Zulip Rudi Grinberg (Jul 01 2022 at 14:17):

(Just about any useful code in OCaml has to allocate)

view this post on Zulip Emilio Jesús Gallego Arias (Jul 01 2022 at 14:17):

I see, we can try that, but last time I checked, long time ago, Coq did starve a lot

view this post on Zulip Emilio Jesús Gallego Arias (Jul 01 2022 at 14:18):

You are using OCaml threads?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 01 2022 at 14:18):

Also, does that work OK on windows?

view this post on Zulip Rudi Grinberg (Jul 01 2022 at 14:19):

It could be a possibility in coq I think. You have your bytecode vm right? is there a way to stop the bytecode vm if it's executing something expensive. That might not necessarily allocate

view this post on Zulip Rudi Grinberg (Jul 01 2022 at 14:19):

I'm using posix threads (threads.posix). The other flavor of ocaml threads (threads.vm) has long been deprecated

view this post on Zulip Rudi Grinberg (Jul 01 2022 at 14:20):

It works quite well on windows as threads are fairly reliable.

view this post on Zulip Rudi Grinberg (Jul 01 2022 at 14:21):

but again, i'm not suggesting that you use threads. I know for merlin it works very well b/c the ocaml frontend will certainly not starve the other threads in the way i mentioned. I have no idea what kind of stuff coq might do

view this post on Zulip Rudi Grinberg (Jul 01 2022 at 14:22):

there is also another practical disadvantage to using threads: you are forced to link against merlin/coq. Which means that you cannot support multiple versions of ocaml/coq in the same server

view this post on Zulip Rudi Grinberg (Jul 01 2022 at 14:22):

i accepted this limitation in lsp b/c merlin has the same limitation anyway

view this post on Zulip Rudi Grinberg (Jul 01 2022 at 14:22):

so users were already used to it

view this post on Zulip Rudi Grinberg (Jul 01 2022 at 14:35):

My hunch would be to start with threads as that is a lot simpler and you don't have to worry about the protocol/process management. Once you run into limitations, you will have a good idea what support you need from the protocol. Then, you should be able to switch to processes easily if the server isn't responsive enough.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 01 2022 at 14:36):

I'll do a test with threads anyways as I'm curious how much Coq starves, but yes, also for other practical purposes we'll have to use processes

view this post on Zulip Emilio Jesús Gallego Arias (Jul 01 2022 at 14:36):

it is hard to really support multiple .v files in the same process due to plugin loading / etc...

view this post on Zulip Rudi Grinberg (Jul 01 2022 at 14:37):

yeah, merlin had to go through a lot of pain repurposing the ocaml typechecker to make it usable for interactive use

view this post on Zulip Rudi Grinberg (Jul 01 2022 at 14:42):

What about supporting multiple versions of coq? Do you plan to do it?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 01 2022 at 15:18):

Not for now

view this post on Zulip Emilio Jesús Gallego Arias (Jul 01 2022 at 15:18):

We have to integrate with Dune first

view this post on Zulip Rudi Grinberg (Jul 01 2022 at 20:39):

Actually I'm not sure how the thread based solution would work on windows. On windows, there's no per thread signal delivery, so how do you expect the coq thread to every be interrupted?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 03 2022 at 21:47):

@Rudi Grinberg , what's the best place to discuss about ocaml-lsp , I got a few questions?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 03 2022 at 21:47):

Do you folks have a Zulip or Slack channel?

view this post on Zulip Rudi Grinberg (Jul 03 2022 at 22:11):

we have a slack for the vscode side of things, but for lsp, you might as well just ask here. I'm the only full time dev on the project.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2022 at 20:56):

Unfortunately lack of Thread.kill prevented us to doing the experiment à la ocaml-lsp-merlin

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2022 at 20:56):

it would have not been perfect, but it would have been a good starting point

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2022 at 20:57):

we will have to spawn a full process and use a protocol + signals

view this post on Zulip Rudi Grinberg (Jul 07 2022 at 03:45):

That's probably for the best anyway

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2022 at 14:29):

Not the best case for us I'm afraid, serialization of Coq stuff remains a huge overhead

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2022 at 14:30):

I did a bit of experiments with serializing the cache more naively, it didn't took long for the Coq state to go from 15MiB to 4GiB due to lack of sharing

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2022 at 14:30):

Coq (like Isabelle and Lean) are really book cases for usual shared memory parallel concurrency

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2022 at 14:30):

proof search

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2022 at 14:31):

Not so different from a chess engine for example

view this post on Zulip Rudi Grinberg (Jul 07 2022 at 14:46):

Why is the cache being serialized though? It seems like only the coq process needs the cache to do whatever its doing faster.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2022 at 14:53):

Sorry, I was serializing the cache to have persistence among the sessions

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2022 at 14:54):

I had to teach Coq's serlib about custom hashing and comparison (so we can ignore AST locations, etc...) that wasn't fun :)

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2022 at 14:55):

Coq also has an extensible AST, so coq-lsp need special support for plugins to work well, so they register their AST properly, that's a hell this system

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2022 at 14:55):

XD

view this post on Zulip Rudi Grinberg (Jul 07 2022 at 14:57):

Why don't you have the coq process understand your "sessions" and then it can do all the caching it wants without serialization.

view this post on Zulip Rudi Grinberg (Jul 07 2022 at 14:58):

That's exactly how it work with lsp/merlin as well btw. Merlin handles its own caches

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2022 at 16:03):

What happens when the Coq process shuts down?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2022 at 16:04):

I was talking about that case, we have a file that takes 90 seconds to process for example, so I'd like when the user opens the file again, we could rebuild

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2022 at 16:04):

actually we got that almost working, see the TODO.org

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2022 at 16:04):

but relying on marhsall that does maximal sharing fo rus

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2022 at 16:04):

for us, but I bet some stupid Ephererons in Coq code are making the marshalling return not the same state

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2022 at 16:05):

so our cache suddently fails, I didn't debug more as it is tricky, but I wrote down in the todo file the problem about it

view this post on Zulip Ali Caglayan (Jul 07 2022 at 16:18):

https://github.com/ejgallego/coq-lsp/blob/main/todo.org

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2022 at 16:58):

That's a bit of same catch 22 we had with the ast comparison, we had to ppx all the AST (which is thousand of types), here for state, we'd need to make all important state points use our cache handles instead of regular OCaml stuff, so we can share in our own cache.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2022 at 16:58):

So that's doable up to some point actually but very tricky work

view this post on Zulip Rudi Grinberg (Jul 07 2022 at 17:01):

Emilio Jesús Gallego Arias said:

What happens when the Coq process shuts down?

If your processes are shutting down, then shared memory will not help you either.

view this post on Zulip Enrico Tassi (Jul 07 2022 at 17:06):

ephemerons were added to identify the data which cannot be marshaled, eg closures. So indeed they drop data.


Last updated: Feb 06 2023 at 05:03 UTC