Allow running load synchronously #137
Conversation
| devShells.default = let | ||
| hsPkgs = pkgs.haskell.packages.${defaultGhcVersion}; | ||
| buildInputs = [ | ||
| hsPkgs.ghc | ||
| hsPkgs.haskell-language-server | ||
| pkgs.cabal-install | ||
| pkgs.hpack | ||
| pkgs.zlib | ||
| ]; | ||
| in pkgs.mkShell { | ||
| buildInputs = buildInputs; | ||
| LD_LIBRARY_PATH = pkgs.lib.makeLibraryPath buildInputs; | ||
| }; |
There was a problem hiding this comment.
This is to allow nix users who don't have a global haskell setup to develop cornelis
|
Is it possible to make a new command that provides the synchronous behavior? That would be preferable in my book. If so, I'd be willing to merge such a change. |
|
As for why your test doesn't work, my suspicion is that even though you're running the vim command synchronously, the connection with Agda is still async. You'll probably need to block until you've got a response from Agda. What that response is? I don't know. But I've found that running agda with |
Yep, that sounds better to me as well, thanks!
Right, thanks for the tip! Side question: Is there some reason why cornelis doesn't automatically expand question marks into metas? This is the behaviour I remember having with emacs, and it's hard to think of a situation where I wouldn't want to expand a question mark into a metas. At least with the synchronous version that blocks the buffer until agda responds to the load command, it seems like there are no downsides to always converting question marks to metas. |
|
From looking at the agda mode for emacs, it seems that you simply can't issue any other commands while agda is loading. They do this by
Does cornelis perhaps want to replicate this behaviour? From looking through the code base, it seems to me that we only indicate an "agda is busy" when we try to issue a But I'm not sure what exactly happens if you try to issue other commands while e.g. agda is currently reloading a file. I would personally wager that there's not much sense in issuing further commands, because by the time agda is done loading, the buffer would potentially be out of date, and you theoretically can't reliable issue any other actions. What's your experience with using cornelis? Do you always wait for |
|
The reason we don't automatically is that it's really hard to implement! The communication between Agda and the editor is rife with race conditions. Emacs gets away with it by embracing the race condition and hacking up a solution that exploits the syntax highlighting of meta variables (when it eventually arrives.) Vim doesn't have nearly as good support for tracking objects in the buffer, and usually gets it wrong.
Pulling out the command gives us a chance to receive the relevant hole information from Agda before needing to process it, which minimizes the chances of this race occurring.
…On February 18, 2024 11:21:31 p.m. PST, Georgi Lyubenov ***@***.***> wrote:
> Is it possible to make a new command that provides the synchronous behavior?
Yep, that sounds better to me as well, thanks!
> You'll probably need to block until you've got a response from Agda.
Right, thanks for the tip!
Side question:
Is there some reason why cornelis doesn't automatically expand question marks into metas? This is the behaviour I remember having with emacs, and it's hard to think of a situation where I *wouldn't* want to expand a question mark into a metas.
At least with the synchronous version that blocks the buffer until agda responds to the load command, it seems like there are no downsides to always converting question marks to metas.
--
Reply to this email directly or view it on GitHub:
#137 (comment)
You are receiving this because you commented.
Message ID: ***@***.***>
|
|
FWIW @googleson78 one thing that occured to me thinking about this work here was that maybe a different way to approach it could be via a callback; so after the results of the I'm not sure if that's significantly easier to implement, but it might be? |
|
The difficult part is
I believe, although I'm not 100% sure. Right now after trying out cornelis for a bit, I'm somewhat convinced the best approach would be to implement the same sort of synchronisation that the emacs agda-mode offers (what I've outlined here), where the whole agda process can be put into a state of "busy" on the nvim plugin side, and then you cannot issue commands while in that state. After that it should also be trivial to block the buffer while the plugin is in the "busy" state. This however obviously will require some bigger amount of work, so I haven't sat down to do it. |
I guess so. Glancing around the code, I suppose what one might need to do is have a kind of Map like Map Response [SomeAction]that gets populated by your special chained command, and when the Agda response comes in ( https://github.com/isovector/cornelis/blob/master/src/Cornelis/Agda.hs#L74 ? ) read that map, and if there is an action in there for the present response, pop it off, and run it. But maybe that's a terribl idea for some reason. Obviously it will fail some race conditions, but probably that won't actually matter if the way it's used is restricted. |
Motivation:
You can't really do much of anything else before agda finishes loading a file, so I'd rather my interface freeze to indicate that the buffer is not in a workable state.
Another big motivation is that if we can rely on load being synchronous, we can then write scripts that run load and rely on the load having completed in order to then run other commands afterwards. Concretely, I wanted to have a bind for
:CornelisLoad<CR>:CornelisQuestionToMeta<CR>, but that doesn't currently work out of the box.Making this PR in a somewhat WIP state since I want to get feedback:
Notably, I'm still not sure this actually makes the command run synchronously, because my example of
:CornelisLoad<CR>:CornelisQuestionToMeta<CR>still doesn't work, but I'm not sure what's going wrong exactly.