search

idris-hackers / idris-mode

Idris syntax highlighting, compiler-supported editing, interactive REPL and more things for Emacs.
GNU General Public License v3.0
268 stars 70 forks source link

Implement Idris 2 proof-search-next IDE Protocol command #510

Closed scotek closed 3 years ago

scotek commented 4 years ago

Idris 2 provides a new protocol command (proof-search-next) to iterate through multiple attempts to solve a hole. It would be nice to support this in idris-mode, especially since Edwin mentions it a lot now in talks.

I don't think it is documented yet but appears in the code (https://github.com/idris-lang/Idris2/blob/14604dcf2d344d225fc1a36e77228e8e99a9d0ec/src/Idris/IDEMode/Commands.idr#L96) and is in at least the Idris vim mode.

scotek commented 4 years ago

I've added my PR that implements this. There is a caveat given in it around having to limit the basic proof-search command for Idris 1 to work around issue #509 though.

jfdm commented 4 years ago

Cool thanks! I am not sure why #509 is happening, and do not have the time to look into that, but I do not see any reason my #511 should not be added.

scotek commented 4 years ago

Ok. Do you want me to remove the now-unused variable code in proof-search-next so it passes the tests? If we eventually figure out why the optional args don't work then we can just revert that single commit to get them back.

jfdm commented 4 years ago

I think it would be reasonable to do that, and also post an email to the mailing list. Someone might be able to help who knows better.

jfdm commented 3 years ago

Fixed in #511