search

idris-hackers / idris-mode

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

Loading file in REPL fails: wrong-type-argument #620

Closed rnikander closed 1 year ago

rnikander commented 1 year ago

I just installed idris2, and idris-mode in my emacs. I ran M-x idris-repl and got a nice looking REPL buffer. Cool. Then I tried to load a file I just wrote:

Idris 0.6.0-55efd7dd7
It typechecks! Ship it!
λΠ> 1+2
3
λΠ> :l "hello.idr"

It errors and I get:

Debugger entered--Lisp error: (wrong-type-argument char-or-string-p nil)
  insert-before-markers(nil)
  idris-repl-insert-result(nil nil)
  #f(compiled-function (g551) #<bytecode 0x19f2269107d74b63>)((:ok nil))
  idris-dispatch-event((:return (:ok nil) 30) #<process Idris IDE support>)
  idris-connection-available-input(#<process Idris IDE support>)
  idris-output-filter(#<process Idris IDE support> "000016(:return (:ok ()) 30)\n")
gallais commented 1 year ago

Note that we don't really have enough maintainers for this to be likely to be fixed anytime soon. In the meantime, you can open the target file in a buffer first and use C-c C-l to load it.