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

Cannot load idris #475

Open colin-adams opened 6 years ago

colin-adams commented 6 years ago

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 commented 6 years ago

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 commented 6 years ago

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 commented 6 years ago

Where do you think the messages should end up?

jsoo1 commented 6 years ago

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

david-christiansen commented 6 years ago

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 commented 6 years ago

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 commented 6 years ago

Looks good. Should we create an issue for it?