Cannot load idris

[colin-adams]

Idris - latest git version idris-mode - freshly installed from melpa with a brand-new .emacs and .emacs.d

.emacs contains:

'(idris-mode-hook (quote (turn-on-idris-simple-indent turn-on-eldoc-mode column-number-mode))) '(package-selected-packages (quote (idris-mode))))

Opening a .idr file puts the buffer into mode Idris (Not loaded)

Pressing C-c C-l results in message: Buffer idris-repl has no process

[jsoo1]

Did you happen to have a package dependency in your ipkg pkgs clause that was not resolved? This happened to me when there was a message Warning from Idris: The following packages were specified but could not be found: - recursion in *Messages*. This is odd becuase I have pkgs = recursion_schemes in the ipkgfile. Note the missing _schemes.

[david-christiansen]

We should definitely set it up so that the messages pop up in a dedicated info buffer instead of going into the Emacs message system.

[jsoo1]

Where do you think the messages should end up?

[jsoo1]

Hmmm. I think I was experiencing #460 but I still like the UX improvement of moving the message to an idris buffer.

[david-christiansen]

I think it would make sense to show them in a *Help*-style buffer. Something like replacing this in inferior-idris.el:

(message "Warning from Idris: %s" msg)

with something like this:

(idris-show-info (format "Warning from Idris during startup:\n %s" msg))

to make it more obvious that it's something the user should know about and perhaps do something about.

[david-christiansen]

This would require pushing some imports around to avoid cycles in the module import graph, but it should be doable. Otherwise, it could be something that just pops up a dedicated non-Idris-info buffer and puts it into read-only mode. Sketch:

(defun idris-show-inferior-idris-warning (msg)
  "Show MSG in a pop-up buffer."
  (let ((buf (get-buffer-create "*Idris Startup Warnings*")))
    (with-current-buffer buf
      (insert msg)
      (terpri)
      (read-only-mode 1))
    (pop-to-buffer buf)))

[jsoo1]

Looks good. Should we create an issue for it?