Better dune support

[lgaeher]

This adds better support for dune, see #344.

Current caveats:

• This blocks when dune needs to compile dependencies. Potentially we could make calling start non-blocking?
• If you create a new unsaved buffer with dependencies from your current project, you will have to save first before starting Coqtail, as otherwise it won't find the dependencies. (this is something which works when using _CoqProject, I think, but isn't a very common occurrence)
• This should have better error reporting. E.g. report that this is a dune project, but dune does not know how to build the file, etc.

For making CoqStart non-blocking, I don't really have any idea how to implement that, but it would be pretty nice to have (or even just emit a message that dependencies are being compiled).
Alternatively, we could also pass --no-build to dune, which skips building the dependencies. That would mirror the current behavior for _CoqProject.

Maybe there should also be a configuration option to enable/disable calling dune at all?

[whonore]

Thanks, this looks like a great start.

This blocks when dune needs to compile dependencies.

I can look into making CoqStart non-blocking. I don't remember right now if there's a technical reason I haven't done this or if there just hasn't been a need for it so far. I think in either case it would make sense to also have an option to enable/disable automatically building dependencies.

Maybe there should also be a configuration option to enable/disable calling dune at all?

I agree. I was thinking something like g:coqtail_use_dune that can be 1 (enable), 0 (disable), or 'auto' (enable if the current or any parent directories have a dune-project file).

If you have the time and interest to continue working on this, feel free, but if not I could take it from here. Just let me know what parts, if any, you want to work on so we don't get in each other's way.

[lgaeher]

Thanks! What you write makes sense.

The remaining tasks all seem to require more advanced vim knowledge than I have, and I'll probably not have too much time in the next two weeks to play with that. So if you're happy to look into that, please feel free to take it from here! Of course, otherwise I'll also be happy to work on that once I get more time.

[lgaeher]

I've got some time to work on this now. I think I'll look into adding the config options you suggested.

[lgaeher]

I added two configuration flags:

• g:coqtail_build_system, which can be dune, coqproject, prefer-coqproject, or prefer-dune. I added details on their behavior to the documentation. (The default is prefer-dune, which matches with the previous behavior of this MR.)
• g:coqtail_dune_compile_deps, which determines whether dune compiles the dependencies before or not.

I also tried to make CoqStart asynchronous. I'm not sure if the way I did it is the best way, so feedback is appreciated.

[lgaeher]

I fixed an issue where stopping Coq (e.g. when dune or coqtop failed to start up correctly) would deadlock vim, due to a reentrancy issue with the channel implementation (?) when invoking CoqStop from the CoqStart callback.
Now CoqStop is also asynchronous.

Another issue I discovered, which I haven't fixed yet, is that commands (like CoqGoToLine) which trigger CoqStart when Coqtail hasn't been started yet, now override the shown error message in case CoqStart failed, as they don't wait for CoqStart to succeed before being sent to the python server.

[whonore]

Thanks a lot, this is looking great so far. I just did a quick pass and made a couple minor notes. I still need to take a closer look and test it more thoroughly, which I'll try to get to soon.

As for the issue with the commands that call coqtail#start(), one option could be to pass them as a callback that only gets called if Coq is started successfully.
So instead of

if s:running() || coqtail#start() | cmd | endif

it could look something like

if s:running() | cmd | else | coqtail#start(string(cmd)) | endif

And then cmd gets passed to coqtail#after_startCB to be executed on success.

[lgaeher]

if s:running() || coqtail#start() | cmd | endif

it could look something like

if s:running() | cmd | else | coqtail#start(string(cmd)) | endif

And then cmd gets passed to coqtail#after_startCB to be executed on success.

Thanks for reviewing! Sounds good, I'll make the change

[lgaeher]

I made the change you suggested, and this seems to work now.
One slightly annoying thing is that it only shows the last line of the error message in the error prompt and you have to do :messages to see the full error message. I don't know how to change that behavior.

Another issue that was introduced by making CoqStop asynchronous is that doing :q while Coqtail is running stops Coqtail, but does not actually quite the buffer. Probably some of the sequencing with disabling the autocmds in CoqStop is wrong, but I can't really figure it out. Maybe you could take a look at this @whonore?
I fixed this issue by changing the sequencing of cleaning up the panels with the callback a bit.

[lgaeher]

Is there anything I can do to make this easier to review (e.g. provide an example dune setup for an example project with instructions how to set it up, provide more documentation, etc.)?

[whonore]

Sorry for the delayed response. I’ve been on vacation, but I’m back now and I’ll try to get to this by this weekend at the latest. Thanks for your patience.

I have some sample projects I can test with, but if you have any test cases or workflows that might help check subtle corner cases, that would be appreciated.

[lgaeher]

Sorry for the delayed response. I’ve been on vacation, but I’m back now and I’ll try to get to this by this weekend at the latest. Thanks for your patience.

Thanks! No worries, hope you had a good vacation.

I have some sample projects I can test with, but if you have any test cases or workflows that might help check subtle corner cases, that would be appreciated.

I mostly tested this on some projects I'm working on, for instance RefinedC.
On these projects, this has worked well the past two months.

I encountered some corner cases recently which we should probably fix:

• if switching the buffer while the asynchronous start is going on, things go wrong, as the after_startCB callback is executed in the context of the wrong buffer
• if calling CoqStop while CoqStart is running and dune is compiling dependencies, the dune process won't be properly stopped and keeps running until it succeeds. Probably we should kill it when receiving a stop signal
• if calling CoqToLine while Coq hasn't started yet, coqtail#toline will be called after the start has happened, and so the current line will be evaluated at that time and not at the time when CoqToLine was called. Probably we should evaluate this earlier in that case.

I'm not sure how to properly fix the first point. Maybe the functions we call in the After_startCB should receive the buffer to execute in as an argument, and then use getbufvar to get the variables in the right scope? Or is there a more elegant way?

[lgaeher]

• if switching the buffer while the asynchronous start is going on, things go wrong, as the after_startCB callback is executed in the context of the wrong buffer

I hacked around this by temporarily switching the buffer in the start callback, which seems to work fine for now: https://github.com/whonore/Coqtail/pull/347/files#diff-12174b01a001d27521768009705e83d295825ed51961111f5edb2f82662a8e3fR457

• if calling CoqStop while CoqStart is running and dune is compiling dependencies, the dune process won't be properly stopped and keeps running until it succeeds. Probably we should kill it when receiving a stop signal

As a first step, I adapted the "interrupt" signal to also terminate the dune process, if it is currently running.
Then, maybe we should just send an "interrupt" to the Python server first when stopping? (or maybe only when Coqtop is has not started already, to not change the existing behaviour?)

[whonore]

This seems to work really well for the most part. Aside from a couple minor style edits I made, I think the only real issue is how the after_start_cmd argument is handled in coqtail#start (see comments).

if switching the buffer while the asynchronous start is going on, things go wrong, as the after_startCB callback is executed in the context of the wrong buffer

I think your solution is good. A couple other parts of the code do basically the same thing to make sure things are executed in the right context.

if calling CoqToLine while Coq hasn't started yet, coqtail#toline will be called after the start has happened, and so the current line will be evaluated at that time and not at the time when CoqToLine was called. Probably we should evaluate this earlier in that case.

This is tricky because CoqToLine passes 0 as the line by default, and then if coqtail#toline sees that, it uses the cursor position, which may have changed since the command was called. I'm inclined to leave this for now and fix it only if it actually turns out to be an issue for people. We'd have to split each command into a "evaluate before CoqStart" and "evaluate after CoqStart" part, which would be annoying and error prone, and it just doesn't seem like that pressing an issue.

if calling CoqStop while CoqStart is running and dune is compiling dependencies, the dune process won't be properly stopped and keeps running until it succeeds. Probably we should kill it when receiving a stop signal

Calling interrupt from coqtail#stop before calling stop might be a good idea. Additionally, Coqtop.stop should probably kill the dune process if self.dune is not None. But the current implementation seems to work well from what I've seen. Interrupting Coq is pretty janky in general.

[lgaeher]

Thanks for the review and the comment!

. I'm inclined to leave this for now and fix it only if it actually turns out to be an issue for people.

Okay, sounds good.

Additionally, Coqtop.stop should probably kill the dune process if self.dune is not None.

I think with the current implementation, the python Coqtop.stop will never be called while dune is running, as the handling of calls in the Python server is synchronous and running dune makes Coqtop.start block. Currently, Coqtop.start will only return once dune has terminated. Hence the suggestion to go via interrupt, which seems to be the only way in the python server to interrupt the current call.

I've implemented this and it seems to work fine. I had to add a b:coqtail_stopping flag to prevent multiple interrupt signals being sent to the Python server while the start is ongoing. (In the case that start is ongoing and waiting for dune and the user calls stop, this would first send an interrupt, which stops dune and makes start fail. Then the after_startCB would call stop again, so we have two interleaved stops going on. That is bad and leads to parts of the cleanupCB to be dropped, etc.)

[whonore]

@lgaeher Great work on this. Everything looks good to me now, so if you can just confirm that it still works on your end after my minor changes I can go ahead and merge it.

[lgaeher]

Yes, looks great! Everything still works for me. Thanks!