ob-idris support?

[zwild]

Hi, thanks for the great work. I want to literate programming with idris. Will idris-mode add ob-idris? Thanks a lot.

[david-christiansen]

We'd almost certainly accept a pull request that made it work! I tried a few years ago but it was taking too long and I gave up.

[dpkatz]

I've been playing with this a bit, and have gotten somewhere but not far enough.

My first attempt was to use comint-mode with the *idris-process* buffer, but that didn't do anything. If I understood what I read, most of the Idris interaction is via a socket rather than through comint.

My second attempt got single line execution going using org-babel-eval with the command line idris -q. Simple evaluation, but no sessions and no multi-line blocks of code:

#+BEGIN_SRC idris :results raw :session none 
3 + 4
#+END_SRC

#+RESULTS:
7 : Integer

My current attempt is to try to get sessions and blocks going. I am trying to use something like

(idris-eval '(:load-file (expand-file-name "~/junk/test.idr")) nil)

where we'd save the contents of the org-babel block to a temp file and then run idris-eval on that. The contents of the test file I'm working with is

import Data.Vect

mymap : (a -> b) -> Vect n a -> Vect n b
mymap f [] = []
mymap f (x :: xs) = f x :: mymap f xs

but if I try to evaluate the elisp directly I get errors:

error in process filter: idris-dispatch-event: Unexpected reply: 66 (:error "parse failure") error in process filter: Unexpected reply: 66 (:error "parse failure")

I'm not sure what that's about or how to diagnose it. If you have any pointers, I'd be happy to keep this moving forward...