idris-mode icon indicating copy to clipboard operation
idris-mode copied to clipboard

Published 20 hours ago • verified publisher icon idris-hackers

loading file with holes causes error

Open bixuanzju opened this issue 9 years ago • 14 comments

Reproduce step:

  1. create a new file

  2. write the following

     test : String
 test = ?hole

  3. run idris-load-file

Debugger info:

Debugger entered--Lisp error: (wrong-type-argument stringp nil) file-name-directory(nil) idris-filename-to-load() idris-update-loaded-region(nil) #257 "\302 \210\303 \210p\304 \235\203�\305 \210\306\307!\210\310!\207" [idris-currently-loaded-buffer idris-warnings-printing idris-make-clean idris-update-options-cache warnings-tree idris-list-compiler-notes run-hooks idris-load-file-success-hook idris-update-loaded-region] 3 "\n\n(fn RESULT)" #257 "\300:\203/@A\301=\204�!\202_\211:\203'\211@A\211\204\211\302:\203@\262\211:\203\211@A:\203 @A:\203@A\303=\203 \211:\203 \211@A\211\204:\203@A:\203@A\304=\203\211:\203\211@A\211:\203\211@A\211\204\377�:\203\377�@A:\203\375�@A\305=\203\373�\211:\203\373�\211@A\211:\203\371�\211@A\211\204\367�\204\367�:\203\367�@A\211\204\365�\306!\306\307 !\230\203\363�\310p &\210\266\266\266\266\266\266\266\266\266\266\266\266\266\266A\262\202&�\302\266\202\262\202"!\266\202\202_!\266\202\2022\211!\207" [#[257 "\302 \210\303 \210p\304 \235\203�\305 \210\306\307!\210\310!\207" [idris-currently-loaded-buffer idris-warnings-printing idris-make-clean idris-update-options-cache warnings-tree idris-list-compiler-notes run-hooks idris-load-file-success-hook idris-update-loaded-region] 3 "\n\n(fn RESULT)"] :highlight-source nil :filename :start :end file-name-nondirectory buffer-file-name idris-highlight-input-region] 48 "\n\n(fn RESULT)" #[1028 "\211\211@A\300\301"\2035�\211\211G\302U\203�\211@\202 �\303\304\305GD"J\2050�Jq\210J!\266\202\202\204�\300\306"\203\200�\211\211\203J�\211A\262\242\202Q�\303\304\305GD"\211A\262\242\203f�\303\304\305\307G\D"\210 J\203w�Jq\210 J!\210\310\311"\266\203\202\204�\312\313"\207" [eql :ok 1 signal wrong-number-of-arguments nil :error 2 message "Evaluation returned an error: %s." error "ELISP destructure-case failed: %S"] 15 "\n\n(fn G69925 G69926 G69927 G69921)"](--failure-cont-- --buffer-- --cont-- %28:ok nil%29) apply(#[1028 "\211\211@A\300\301"\2035�\211\211G\302U\203�\211@\202 �\303\304\305GD"J\2050�Jq\210J!\266\202\202\204�\300\306"\203\200�\211\211\203J�\211A\262\242\202Q�\303\304\305GD"\211A\262\242\203f�\303\304\305\307G\D"\210 J\203w�Jq\210 J!\210\310\311"\266\203\202\204�\312\313"\207" [eql :ok 1 signal wrong-number-of-arguments nil :error 2 message "Evaluation returned an error: %s." error "ELISP destructure-case failed: %S"] 15 "\n\n(fn G69925 G69926 G69927 G69921)"] --failure-cont-- --buffer-- --cont-- (:ok nil)) (lambda (&rest --cl-rest--) (apply (quote #[1028 "\211\211@A\300\301"\2035�\211\211G\302U\203�\211@\202 �\303\304\305GD"J\2050�Jq\210J!\266\202\202\204�\300\306"\203\200�\211\211\203J�\211A\262\242\202Q�\303\304\305GD"\211A\262\242\203f�\303\304\305\307G\D"\210 J\203w�Jq\210 J!\210\310\311"\266\203\202\204�\312\313"\207" [eql :ok 1 signal wrong-number-of-arguments nil :error 2 message "Evaluation returned an error: %s." error "ELISP destructure-case failed: %S"] 15 "\n\n(fn G69925 G69926 G69927 G69921)"]) (quote --failure-cont--) (quote --buffer--) (quote --cont--) --cl-rest--))((:ok nil)) idris-dispatch-event((:return (:ok nil) 42) #<process Idris IDE support>) idris-connection-available-input(#<process Idris IDE support>) idris-output-filter(#<process Idris IDE support> "00001a(:set-prompt "*hello" 42)\n000016(:return (:ok ()) 42)\n")

bixuanzju avatar Apr 12 '16 08:04 bixuanzju

thanks for the report, could you please indicate which versions of idris and idris-mode you're using?

hannesm avatar Apr 12 '16 08:04 hannesm

@hannesm idris version 0.11, I installed idris-mode from MELPA

bixuanzju avatar Apr 12 '16 09:04 bixuanzju

thx, hope @david-christiansen (or someone else) will jump in now (sorry, I currently don't have any idris installed)

hannesm avatar Apr 12 '16 09:04 hannesm

@hannesm Any update on this? Thank you!

bixuanzju avatar Apr 26 '16 07:04 bixuanzju

No one ever see this error?

bixuanzju avatar Nov 02 '16 01:11 bixuanzju

I'm not able to reproduce this. Is it still happening for you on the latest version?

david-christiansen avatar Dec 29 '16 07:12 david-christiansen

Looking at the backtrace, it seems to occur because idris-mode can't find the filename for your buffer.

Can you please check if this branch solves the problem for you? I'd do it, but I haven't yet reproduced the error myself: https://github.com/david-christiansen/idris-mode/tree/issue/423

Thanks for your patience!

david-christiansen avatar Dec 29 '16 07:12 david-christiansen

@david-christiansen sorry for the last reply. The problem still persists, though with different error message:

Debugger entered--Lisp error: (error "Buffer is not visiting a file")
  signal(error ("Buffer is not visiting a file"))
  error("Buffer is not visiting a file")
  (if fn fn (error "Buffer is not visiting a file"))
  (let ((fn (buffer-file-name buffer))) (if fn fn (error "Buffer is not visiting a file")))
  idris-buffer-file-name()
  (let* ((fn (idris-buffer-file-name)) (ipkg-srcdir (idris-ipkg-find-src-dir)) (srcdir (if ipkg-srcdir ipkg-srcdir (file-name-directory fn)))) (if (and (> (length fn) (length srcdir)) (string= (substring fn 0 (length srcdir)) srcdir)) (progn (setq fn (file-relative-name fn srcdir)))) (cons srcdir fn))
  idris-filename-to-load()
  (cdr (idris-filename-to-load))
  (list (quote :filename) (cdr (idris-filename-to-load)))
  (list (list (quote :filename) (cdr (idris-filename-to-load))) (quote (:start 1 1)) (save-excursion (goto-char (point-max)) (cons (quote :end) (cons (idris-get-line-num) (quote (1))))))
  (idris-update-loaded-region (list (list (quote :filename) (cdr (idris-filename-to-load))) (quote (:start 1 1)) (save-excursion (goto-char (point-max)) (cons (quote :end) (cons (idris-get-line-num) (quote (1)))))))
  (if fc (let* ((end (assoc :end fc)) (line (car (cdr end))) (col (car (cdr (cdr end))))) (if (overlayp idris-loaded-region-overlay) (progn (delete-overlay idris-loaded-region-overlay))) (save-current-buffer (set-buffer idris-currently-loaded-buffer) (setq idris-loaded-region-overlay (make-overlay (point-min) (save-excursion (goto-char (point-min)) (forward-line (1- line)) (move-to-column (1- col)) (point)) (current-buffer))) (overlay-put idris-loaded-region-overlay (quote face) (quote idris-loaded-region-face)))) (idris-update-loaded-region (list (list (quote :filename) (cdr (idris-filename-to-load))) (quote (:start 1 1)) (save-excursion (goto-char (point-max)) (cons (quote :end) (cons (idris-get-line-num) (quote (1))))))))
  idris-update-loaded-region(nil)
  (closure ((result) (srcdir . "/Users/jeremybi/scratch/") (fn . "test.idr") (dir-and-fn "/Users/jeremybi/scratch/" . "test.idr") (set-line . 1) t) nil (idris-make-clean) (idris-update-options-cache) (setq idris-currently-loaded-buffer (current-buffer)) (if (member (quote warnings-tree) idris-warnings-printing) (progn (idris-list-compiler-notes))) (run-hooks (quote idris-load-file-success-hook)) (idris-update-loaded-region result))()
  funcall((closure ((result) (srcdir . "/Users/jeremybi/scratch/") (fn . "test.idr") (dir-and-fn "/Users/jeremybi/scratch/" . "test.idr") (set-line . 1) t) nil (idris-make-clean) (idris-update-options-cache) (setq idris-currently-loaded-buffer (current-buffer)) (if (member (quote warnings-tree) idris-warnings-printing) (progn (idris-list-compiler-notes))) (run-hooks (quote idris-load-file-success-hook)) (idris-update-loaded-region result)))
  (if (consp result) (let* ((x (car result))) (if (eq x :highlight-source) (let* ((x (cdr result))) (if (consp x) (let* ((x ...) (x ...)) (if (null x) (let ... ...) (funcall pcase-0))) (funcall pcase-0))) (funcall pcase-0))) (funcall pcase-0))
  (let* ((pcase-0 (function (lambda nil (idris-make-clean) (idris-update-options-cache) (setq idris-currently-loaded-buffer (current-buffer)) (if (member (quote warnings-tree) idris-warnings-printing) (progn (idris-list-compiler-notes))) (run-hooks (quote idris-load-file-success-hook)) (idris-update-loaded-region result))))) (if (consp result) (let* ((x (car result))) (if (eq x :highlight-source) (let* ((x (cdr result))) (if (consp x) (let* (... ...) (if ... ... ...)) (funcall pcase-0))) (funcall pcase-0))) (funcall pcase-0)))
  (closure ((srcdir . "/Users/jeremybi/scratch/") (fn . "test.idr") (dir-and-fn "/Users/jeremybi/scratch/" . "test.idr") (set-line . 1) t) (result) (let* ((pcase-0 (function (lambda nil (idris-make-clean) (idris-update-options-cache) (setq idris-currently-loaded-buffer (current-buffer)) (if (member ... idris-warnings-printing) (progn ...)) (run-hooks (quote idris-load-file-success-hook)) (idris-update-loaded-region result))))) (if (consp result) (let* ((x (car result))) (if (eq x :highlight-source) (let* ((x ...)) (if (consp x) (let* ... ...) (funcall pcase-0))) (funcall pcase-0))) (funcall pcase-0))))(nil)
  funcall((closure ((srcdir . "/Users/jeremybi/scratch/") (fn . "test.idr") (dir-and-fn "/Users/jeremybi/scratch/" . "test.idr") (set-line . 1) t) (result) (let* ((pcase-0 (function (lambda nil (idris-make-clean) (idris-update-options-cache) (setq idris-currently-loaded-buffer (current-buffer)) (if (member ... idris-warnings-printing) (progn ...)) (run-hooks (quote idris-load-file-success-hook)) (idris-update-loaded-region result))))) (if (consp result) (let* ((x (car result))) (if (eq x :highlight-source) (let* ((x ...)) (if (consp x) (let* ... ...) (funcall pcase-0))) (funcall pcase-0))) (funcall pcase-0)))) nil)
  (progn (set-buffer (symbol-value G365)) (funcall (symbol-value G366) result))
  (if (symbol-value G366) (progn (set-buffer (symbol-value G365)) (funcall (symbol-value G366) result)))
  (let* ((--cl-rest-- rand-362) (result (if (= (length --cl-rest--) 1) (car --cl-rest--) (signal (quote wrong-number-of-arguments) (list nil (length --cl-rest--)))))) (if (symbol-value G366) (progn (set-buffer (symbol-value G365)) (funcall (symbol-value G366) result))))
  (cond ((eql op-361 (quote :ok)) (let* ((--cl-rest-- rand-362) (result (if (= (length --cl-rest--) 1) (car --cl-rest--) (signal (quote wrong-number-of-arguments) (list nil ...))))) (if (symbol-value G366) (progn (set-buffer (symbol-value G365)) (funcall (symbol-value G366) result))))) ((eql op-361 (quote :error)) (let* ((--cl-rest-- rand-362) (condition (if --cl-rest-- (car-safe (prog1 --cl-rest-- ...)) (signal (quote wrong-number-of-arguments) (list nil ...)))) (_spans (car-safe (prog1 --cl-rest-- (setq --cl-rest-- ...))))) (progn (if --cl-rest-- (signal (quote wrong-number-of-arguments) (list nil (+ 2 ...)))) (if (symbol-value G364) (progn (set-buffer (symbol-value G365)) (funcall (symbol-value G364) condition))) (message "Evaluation returned an error: %s." condition)))) (t (error "ELISP destructure-case failed: %S" tmp-363)))
  (let* ((tmp-363 G360) (op-361 (car tmp-363)) (rand-362 (cdr tmp-363))) (cond ((eql op-361 (quote :ok)) (let* ((--cl-rest-- rand-362) (result (if (= ... 1) (car --cl-rest--) (signal ... ...)))) (if (symbol-value G366) (progn (set-buffer (symbol-value G365)) (funcall (symbol-value G366) result))))) ((eql op-361 (quote :error)) (let* ((--cl-rest-- rand-362) (condition (if --cl-rest-- (car-safe ...) (signal ... ...))) (_spans (car-safe (prog1 --cl-rest-- ...)))) (progn (if --cl-rest-- (signal (quote wrong-number-of-arguments) (list nil ...))) (if (symbol-value G364) (progn (set-buffer ...) (funcall ... condition))) (message "Evaluation returned an error: %s." condition)))) (t (error "ELISP destructure-case failed: %S" tmp-363))))
  (closure ((--cl-failure-cont-- . --failure-cont--) (--cl-buffer-- . --buffer--) (--cl-cont-- . --cont--) (failure-cont closure ((srcdir . "/Users/jeremybi/scratch/") (fn . "test.idr") (dir-and-fn "/Users/jeremybi/scratch/" . "test.idr") (set-line . 1) t) (_condition) (if (member (quote warnings-tree) idris-warnings-printing) (progn (idris-list-compiler-notes) (pop-to-buffer (idris-buffer-name :notes))))) (cont closure ((srcdir . "/Users/jeremybi/scratch/") (fn . "test.idr") (dir-and-fn "/Users/jeremybi/scratch/" . "test.idr") (set-line . 1) t) (result) (let* ((pcase-0 (function (lambda nil ... ... ... ... ... ...)))) (if (consp result) (let* ((x ...)) (if (eq x :highlight-source) (let* ... ...) (funcall pcase-0))) (funcall pcase-0)))) (sexp :load-file "test.idr") idris-event-hooks t) (G364 G365 G366 G360) (let* ((tmp-363 G360) (op-361 (car tmp-363)) (rand-362 (cdr tmp-363))) (cond ((eql op-361 (quote :ok)) (let* ((--cl-rest-- rand-362) (result (if ... ... ...))) (if (symbol-value G366) (progn (set-buffer ...) (funcall ... result))))) ((eql op-361 (quote :error)) (let* ((--cl-rest-- rand-362) (condition (if --cl-rest-- ... ...)) (_spans (car-safe ...))) (progn (if --cl-rest-- (signal ... ...)) (if (symbol-value G364) (progn ... ...)) (message "Evaluation returned an error: %s." condition)))) (t (error "ELISP destructure-case failed: %S" tmp-363)))))(--failure-cont-- --buffer-- --cont-- (:ok nil))
  apply((closure ((--cl-failure-cont-- . --failure-cont--) (--cl-buffer-- . --buffer--) (--cl-cont-- . --cont--) (failure-cont closure ((srcdir . "/Users/jeremybi/scratch/") (fn . "test.idr") (dir-and-fn "/Users/jeremybi/scratch/" . "test.idr") (set-line . 1) t) (_condition) (if (member (quote warnings-tree) idris-warnings-printing) (progn (idris-list-compiler-notes) (pop-to-buffer (idris-buffer-name :notes))))) (cont closure ((srcdir . "/Users/jeremybi/scratch/") (fn . "test.idr") (dir-and-fn "/Users/jeremybi/scratch/" . "test.idr") (set-line . 1) t) (result) (let* ((pcase-0 (function (lambda nil ... ... ... ... ... ...)))) (if (consp result) (let* ((x ...)) (if (eq x :highlight-source) (let* ... ...) (funcall pcase-0))) (funcall pcase-0)))) (sexp :load-file "test.idr") idris-event-hooks t) (G364 G365 G366 G360) (let* ((tmp-363 G360) (op-361 (car tmp-363)) (rand-362 (cdr tmp-363))) (cond ((eql op-361 (quote :ok)) (let* ((--cl-rest-- rand-362) (result (if ... ... ...))) (if (symbol-value G366) (progn (set-buffer ...) (funcall ... result))))) ((eql op-361 (quote :error)) (let* ((--cl-rest-- rand-362) (condition (if --cl-rest-- ... ...)) (_spans (car-safe ...))) (progn (if --cl-rest-- (signal ... ...)) (if (symbol-value G364) (progn ... ...)) (message "Evaluation returned an error: %s." condition)))) (t (error "ELISP destructure-case failed: %S" tmp-363))))) --failure-cont-- --buffer-- --cont-- (:ok nil))
  (lambda (&rest --cl-rest--) (apply (quote (closure ((--cl-failure-cont-- . --failure-cont--) (--cl-buffer-- . --buffer--) (--cl-cont-- . --cont--) (failure-cont closure ((srcdir . "/Users/jeremybi/scratch/") (fn . "test.idr") (dir-and-fn "/Users/jeremybi/scratch/" . "test.idr") (set-line . 1) t) (_condition) (if (member ... idris-warnings-printing) (progn ... ...))) (cont closure ((srcdir . "/Users/jeremybi/scratch/") (fn . "test.idr") (dir-and-fn "/Users/jeremybi/scratch/" . "test.idr") (set-line . 1) t) (result) (let* (...) (if ... ... ...))) (sexp :load-file "test.idr") idris-event-hooks t) (G364 G365 G366 G360) (let* ((tmp-363 G360) (op-361 (car tmp-363)) (rand-362 (cdr tmp-363))) (cond ((eql op-361 ...) (let* ... ...)) ((eql op-361 ...) (let* ... ...)) (t (error "ELISP destructure-case failed: %S" tmp-363)))))) (quote --failure-cont--) (quote --buffer--) (quote --cont--) --cl-rest--))((:ok nil))
  funcall((lambda (&rest --cl-rest--) (apply (quote (closure ((--cl-failure-cont-- . --failure-cont--) (--cl-buffer-- . --buffer--) (--cl-cont-- . --cont--) (failure-cont closure ((srcdir . "/Users/jeremybi/scratch/") (fn . "test.idr") (dir-and-fn "/Users/jeremybi/scratch/" . "test.idr") (set-line . 1) t) (_condition) (if (member ... idris-warnings-printing) (progn ... ...))) (cont closure ((srcdir . "/Users/jeremybi/scratch/") (fn . "test.idr") (dir-and-fn "/Users/jeremybi/scratch/" . "test.idr") (set-line . 1) t) (result) (let* (...) (if ... ... ...))) (sexp :load-file "test.idr") idris-event-hooks t) (G364 G365 G366 G360) (let* ((tmp-363 G360) (op-361 (car tmp-363)) (rand-362 (cdr tmp-363))) (cond ((eql op-361 ...) (let* ... ...)) ((eql op-361 ...) (let* ... ...)) (t (error "ELISP destructure-case failed: %S" tmp-363)))))) (quote --failure-cont--) (quote --buffer--) (quote --cont--) --cl-rest--)) (:ok nil))
  (cond (rec (setq idris-rex-continuations (remove rec idris-rex-continuations)) (funcall (car (cdr rec)) value)) (t (error "Unexpected reply: %S %S" id value)))
  (let ((rec (assq id idris-rex-continuations))) (cond (rec (setq idris-rex-continuations (remove rec idris-rex-continuations)) (funcall (car (cdr rec)) value)) (t (error "Unexpected reply: %S %S" id value))))
  (let* ((--cl-rest-- rand-358) (value (if (= (length --cl-rest--) 2) (car-safe (prog1 --cl-rest-- (setq --cl-rest-- (cdr --cl-rest--)))) (signal (quote wrong-number-of-arguments) (list nil (length --cl-rest--))))) (id (car --cl-rest--))) (let ((rec (assq id idris-rex-continuations))) (cond (rec (setq idris-rex-continuations (remove rec idris-rex-continuations)) (funcall (car (cdr rec)) value)) (t (error "Unexpected reply: %S %S" id value)))))
  (cond ((eql op-357 (quote :emacs-rex)) (let* ((--cl-rest-- rand-358) (form (if (cdr --cl-rest--) (car-safe (prog1 --cl-rest-- ...)) (signal (quote wrong-number-of-arguments) (list nil ...)))) (continuation (car-safe (prog1 --cl-rest-- (setq --cl-rest-- ...)))) (output-continuation (car-safe (prog1 --cl-rest-- (setq --cl-rest-- ...))))) (progn (if --cl-rest-- (signal (quote wrong-number-of-arguments) (list nil (+ 3 ...)))) (let ((id (setq idris-continuation-counter ...))) (idris-send (list form id) process) (setq idris-rex-continuations (cons (if output-continuation ... ...) idris-rex-continuations)))))) ((eql op-357 (quote :output)) (let* ((--cl-rest-- rand-358) (value (if (= (length --cl-rest--) 2) (car-safe (prog1 --cl-rest-- ...)) (signal (quote wrong-number-of-arguments) (list nil ...)))) (id (car --cl-rest--))) (let ((rec (assq id idris-rex-continuations))) (if (and rec (nth 2 rec)) (progn (funcall (nth 2 rec) value)))))) ((eql op-357 (quote :return)) (let* ((--cl-rest-- rand-358) (value (if (= (length --cl-rest--) 2) (car-safe (prog1 --cl-rest-- ...)) (signal (quote wrong-number-of-arguments) (list nil ...)))) (id (car --cl-rest--))) (let ((rec (assq id idris-rex-continuations))) (cond (rec (setq idris-rex-continuations (remove rec idris-rex-continuations)) (funcall (car ...) value)) (t (error "Unexpected reply: %S %S" id value)))))) (t (error "ELISP destructure-case failed: %S" tmp-359)))
  (let* ((tmp-359 event) (op-357 (car tmp-359)) (rand-358 (cdr tmp-359))) (cond ((eql op-357 (quote :emacs-rex)) (let* ((--cl-rest-- rand-358) (form (if (cdr --cl-rest--) (car-safe ...) (signal ... ...))) (continuation (car-safe (prog1 --cl-rest-- ...))) (output-continuation (car-safe (prog1 --cl-rest-- ...)))) (progn (if --cl-rest-- (signal (quote wrong-number-of-arguments) (list nil ...))) (let ((id ...)) (idris-send (list form id) process) (setq idris-rex-continuations (cons ... idris-rex-continuations)))))) ((eql op-357 (quote :output)) (let* ((--cl-rest-- rand-358) (value (if (= ... 2) (car-safe ...) (signal ... ...))) (id (car --cl-rest--))) (let ((rec (assq id idris-rex-continuations))) (if (and rec (nth 2 rec)) (progn (funcall ... value)))))) ((eql op-357 (quote :return)) (let* ((--cl-rest-- rand-358) (value (if (= ... 2) (car-safe ...) (signal ... ...))) (id (car --cl-rest--))) (let ((rec (assq id idris-rex-continuations))) (cond (rec (setq idris-rex-continuations ...) (funcall ... value)) (t (error "Unexpected reply: %S %S" id value)))))) (t (error "ELISP destructure-case failed: %S" tmp-359))))
  (or (run-hook-with-args-until-success (quote idris-event-hooks) event) (let* ((tmp-359 event) (op-357 (car tmp-359)) (rand-358 (cdr tmp-359))) (cond ((eql op-357 (quote :emacs-rex)) (let* ((--cl-rest-- rand-358) (form (if ... ... ...)) (continuation (car-safe ...)) (output-continuation (car-safe ...))) (progn (if --cl-rest-- (signal ... ...)) (let (...) (idris-send ... process) (setq idris-rex-continuations ...))))) ((eql op-357 (quote :output)) (let* ((--cl-rest-- rand-358) (value (if ... ... ...)) (id (car --cl-rest--))) (let ((rec ...)) (if (and rec ...) (progn ...))))) ((eql op-357 (quote :return)) (let* ((--cl-rest-- rand-358) (value (if ... ... ...)) (id (car --cl-rest--))) (let ((rec ...)) (cond (rec ... ...) (t ...))))) (t (error "ELISP destructure-case failed: %S" tmp-359)))))
  idris-dispatch-event((:return (:ok nil) 9) #<process Idris IDE support>)
  (save-current-buffer (idris-dispatch-event event process))
  (unwind-protect (save-current-buffer (idris-dispatch-event event process)))
  (let ((event (idris-receive))) (idris-event-log event nil) (unwind-protect (save-current-buffer (idris-dispatch-event event process))))
  (while (idris-have-input-p) (let ((event (idris-receive))) (idris-event-log event nil) (unwind-protect (save-current-buffer (idris-dispatch-event event process)))))
  (save-current-buffer (set-buffer (process-buffer process)) (while (idris-have-input-p) (let ((event (idris-receive))) (idris-event-log event nil) (unwind-protect (save-current-buffer (idris-dispatch-event event process))))))
  idris-connection-available-input(#<process Idris IDE support>)
  idris-output-filter(#<process Idris IDE support> "000018(:set-prompt \"*test\" 9)\n000015(:return (:ok ()) 9)\n")

I am pretty sure the file i am editing is named "test.idr"

bixuanzju avatar Sep 24 '17 03:09 bixuanzju

I'll add that I'm getting the same error. I'm on spacemacs, so I'm using idris-mode via the spacemacs idris layer. Whenever I call idris-load-file on a file with holes, I get this error message:

error in process filter: idris-filename-to-load: Wrong type argument: stringp, nil
error in process filter: Wrong type argument: stringp, nil

If I (trace-function 'idris-load-file), I get the following when the error occurs:

1 -> (idris-load-file 1)
1 <- idris-load-file: ((416 (lambda #1=(&rest --cl-rest--) (apply (quote #[1028 "\211\211@A\300\301\"\2035�\211\211G\302U\203�\211@\202 �\303\304\305GD\"J\2050�Jq\210J!\266\202\202\204�\300\306\"\203\200�\211\211\203J�\211A\262\242\202Q�\303\304\305GD\"\211A\262\242\203f�\303\304\305\307G\\D\"\210	J\203w�Jq\210	J!\210\310\311\"\266\203\202\204�\312\313\"\207" [eql :ok 1 signal wrong-number-of-arguments nil :error 2 message #2="Evaluation returned an error: %s." error #3="ELISP destructure-case failed: %S"] 15 "

(fn G102 G103 G104 G98)"]) (quote --failure-cont--) (quote --buffer--) (quote --cont--) --cl-rest--)) (lambda #1# (apply (quote #[1028 "\211\211@A\300\301\"\2035�\211\211G\302U\203�\211@\202 �\303\304\305GD\"J\2050�Jq\210J!\266\202\202\204�\300\306\"\203\200�\211\211\203J�\211A\262\242\202Q�\303\304\305GD\"\211A\262\242\203f�\303\304\305\307G\\D\"\210	J\203w�Jq\210	J!\210\310\311\"\266\203\202\204�\312\313\"\207" [eql :ok 1 signal wrong-number-of-arguments nil :error 2 message #2# error #3#] 15 "

(fn G108 G109 G110 G98)"]) (quote --failure-cont--) (quote --buffer--) (quote --cont--) --cl-rest--))))

The *idris-holes buffer does eventually come up, but there's a 3-4 second delay, which is long enough to break flow. (ignore-errors (idris-load-file)) doesn't eliminate it, unfortunately (I don't have deep enough knowledge of emacs lisp to know why -- maybe because it's some sort of secondary process?).

Any fixes (or workarounds) much appreciated! I can refile this as a new issue if y'all would prefer, since this issue is closed.

eggsyntax avatar Jun 10 '18 18:06 eggsyntax

I am experiencing this in spacemacs as well with idris 1.3.0:

Debugger entered--Lisp error: (wrong-type-argument stringp nil)
  file-name-directory(nil)
  idris-filename-to-load()
  idris-update-loaded-region(nil)
  #f(compiled-function (result) #<bytecode 0x43bce415>)(nil)
  #f(compiled-function (result) #<bytecode 0x43bce449>)(nil)
  #f(compiled-function (g492 g493 g494 g488) #<bytecode 0x415419cd>)(--failure-cont-- --buffer-- --cont-- (:ok nil))
  apply(#f(compiled-function (g492 g493 g494 g488) #<bytecode 0x415419cd>) --failure-cont-- --buffer-- --cont-- (:ok nil))
  (lambda (&rest --cl-rest--) (apply (function #f(compiled-function (g492 g493 g494 g488) #<bytecode 0x415419cd>)) '--failure-cont-- '--buffer-- '--cont-- --cl-rest--))((:ok nil))
  idris-dispatch-event((:return (:ok nil) 9) #<process Idris IDE support>)
  idris-connection-available-input(#<process Idris IDE support>)
  idris-output-filter(#<process Idris IDE support> "000018(:set-prompt \"*Poem\" 9)\n000015(:return (:ok ()) 9)\n")

jsoo1 avatar Jul 23 '18 19:07 jsoo1

Can the issue be reopened since multiple people are experiencing it?

jsoo1 avatar Jul 23 '18 19:07 jsoo1

I did some initial debugging and it looks loading a file in spacemacs focuses on the holes buffer immediately. Then (buffer-file-name) returns nil when checking (idris-filename-to-load). Should I report in spacemacs or keep the issue here? It seems like using buffer-file-name for this purpose may not be the most robust thing.

jsoo1 avatar Jul 28 '18 19:07 jsoo1

I put in a PR at spacemacs: https://github.com/syl20bnr/spacemacs/pull/11098 . Will that suffice for idris-mode, or is more work required?

jsoo1 avatar Jul 28 '18 19:07 jsoo1

The spacemacs PR mentioned trying to fix in idris-mode. I tend to think they should be fixed in both places. Certainly there must be a better way to get the file to load other than the stateful buffer-file-name. Is there any reason we can't capture the file name to load in a let binding or use lexical scoping to make the buffer calculation more pure?

jsoo1 avatar Jul 29 '18 18:07 jsoo1