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!
Note that I run merlin in a separate thread - not a process. This saves me some latency although I doubt it’s essential
I do manage the ocamlformat processes in a similar way though and it seems to work fine
The cancellation scheme you describe seems sensible to me
Ah! Indeed that saves some latency, I was confused indeed.
So if merlin hangs, the whole ocaml-lsp server hangs?
Yes I saw ocamlformat was doing differently, I'll have a look thanks
@Ali Caglayan told me that lev should works better for us than lwt, right?
but do you have a lev release on opam or should we just vendor it?
If merlin hangs, only the thread dedicated to merlin hangs.
But merlin never hangs, just serves some requests slowly
However the lsp server remains responsive throughout
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.
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
?
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.
Yeah I had a look and indeed looks pretty nice I think, tho I'm not an expert
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.
In theory, one thread can starve the other by having some infinite loop that never allocates. But this never happens in practice
(Just about any useful code in OCaml has to allocate)
I see, we can try that, but last time I checked, long time ago, Coq did starve a lot
You are using OCaml threads?
Also, does that work OK on windows?
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
I'm using posix threads (threads.posix
). The other flavor of ocaml threads (threads.vm
) has long been deprecated
It works quite well on windows as threads are fairly reliable.
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
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
i accepted this limitation in lsp b/c merlin has the same limitation anyway
so users were already used to it
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.
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
it is hard to really support multiple .v files in the same process due to plugin loading / etc...
yeah, merlin had to go through a lot of pain repurposing the ocaml typechecker to make it usable for interactive use
What about supporting multiple versions of coq? Do you plan to do it?
Not for now
We have to integrate with Dune first
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 ever be interrupted?
@Rudi Grinberg , what's the best place to discuss about ocaml-lsp , I got a few questions?
Do you folks have a Zulip or Slack channel?
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.
Unfortunately lack of Thread.kill
prevented us to doing the experiment à la ocaml-lsp-merlin
it would have not been perfect, but it would have been a good starting point
we will have to spawn a full process and use a protocol + signals
That's probably for the best anyway
Not the best case for us I'm afraid, serialization of Coq stuff remains a huge overhead
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
Coq (like Isabelle and Lean) are really book cases for usual shared memory parallel concurrency
proof search
Not so different from a chess engine for example
Why is the cache being serialized though? It seems like only the coq process needs the cache to do whatever its doing faster.
Sorry, I was serializing the cache to have persistence among the sessions
I had to teach Coq's serlib about custom hashing and comparison (so we can ignore AST locations, etc...) that wasn't fun :)
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
XD
Why don't you have the coq process understand your "sessions" and then it can do all the caching it wants without serialization.
That's exactly how it work with lsp/merlin as well btw. Merlin handles its own caches
What happens when the Coq process shuts down?
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
actually we got that almost working, see the TODO.org
but relying on marhsall that does maximal sharing fo rus
for us, but I bet some stupid Ephererons in Coq code are making the marshalling return not the same state
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
https://github.com/ejgallego/coq-lsp/blob/main/todo.org
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.
So that's doable up to some point actually but very tricky work
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.
ephemerons were added to identify the data which cannot be marshaled, eg closures. So indeed they drop data.
Last updated: Mar 28 2024 at 20:01 UTC