agda-vim
agda-vim copied to clipboard
derekelkins
(Seemingly) fail to handle multiple responses from Agsy
I noticed that when Agsy seems to synthesize solutions to multiple holes (possibly due to some hole being a parameter to the type of another hole), agda-vim appears no be surprised and may put the generated terms into wrong holes or ignore some of them. (Sorry I have not spent the time debugging, verifying the raw output from Agsy or studying the relevant code.)
I'm pretty sure I don't handle this because I don't think I've seen this happen. Can you provide a simple example and the version of Agda you're using? It doesn't need to be a minimal example, just preferably something that's reasonably self-contained.
Yes I will (should) try to create an example. In the meanwhile I vaguely remember the message looks like this: https://github.com/agda/agda/blob/master/src/full/Agda/Auto/Auto.hs#L335. Hope this helps.
Sorry it seems I failed to preserve the work in progress that would trigger the message. (Those files were finished and putting holes back now has not been successful.) I will come back if I see the message again.
Okay, I'll try to reverse engineer an example based on what the Agda/Agsy code is.
Closing this as I'm no longer using this great plug-in and no one else is reporting the same problem.