error in process filter: Wrong type argument: sequencep, 78

gergoerdi commented 2 years ago

With Idris2 0.5.1 and idris-mode 20210728.846, I get the following error whenever I load a file with C-c C-l:

error in process filter: Wrong type argument: sequencep, 78

Emacs version: GNU Emacs 26.3 (build 2, x86_64-pc-linux-gnu, GTK+ Version 3.24.14) of 2020-03-26, modified by Debian

gallais commented 2 years ago

This means some message sent to emacs is malformed. In the meantime you can use https://github.com/idris-community/idris2-mode/

gergoerdi commented 2 years ago

Well then it seems I am shit out of luck:

make in a fresh checkout of idris2-mode fails with:

emacs --batch --no-site-file -q -eval '(add-to-list (quote load-path) "idris2-mode/")' -eval '(require (quote package))' -eval '(add-to-list (quote package-archives) (quote ("melpa" . "http://melpa.org/packages/")) t)' -eval '(package-initialize)' -eval '(progn (require (quote bytecomp)) (setq byte-compile-warnings t) (setq byte-compile-error-on-warn t))' -f batch-byte-compile idris2-commands.el

In toplevel form:
idris2-commands.el:365:1:Error: Unused lexical variable ‘name’

Loading idris2-mode without building then results in the same error message Wrong argument type: sequencep, 78 on C-c C-l
Where it gets spicy: the idris2-mode repo has no issue tracker so there is no one to contact on this problem...

gergoerdi commented 2 years ago

I can reproduce this with just the following cut-down ~/.emacs:

(package-initialize)

(add-to-list 'load-path "~/.emacs.d/elisp/idris2-mode")
(require 'idris2-mode)

(custom-set-variables
 '(idris2-interpreter-path "~/.idris2/bin/idris2"))

gallais commented 2 years ago

make in a fresh checkout of idris2-mode fails with:

I've never tried to run make, I have no idea what it does. This is all that's needed AFAIK (which is more or less what the README says):

(add-to-list 'load-path "PATH_TO_/idris2-mode/")
(require 'idris2-mode)
(add-to-list 'auto-mode-alist '("\\.idr\\'" . idris2-mode))

gergoerdi commented 2 years ago

I've never tried to run make, I have no idea what it does.

Right. It is a red herring anyway -- as I put in this comment, I get the sequencep failure even with a minimal .emacs. (I am surprised it works for you without (package-initialize) tbh because then prop-menu should be an unresolved reference)

So the real problem to concentrate on here is the original one -- that both on idris-mode and idris2-mode, loading a file fails with an error message.

gallais commented 2 years ago

both on idris-mode and idris2-mode, loading a file fails with an error message.

Very strange. Can you run idris2 in a terminal? Does it correctly open a REPL for you?

gergoerdi commented 2 years ago

Very strange. Can you run idris2 in a terminal? Does it correctly open a REPL for you?

Yes; in fact, that's the only way I can run Idris2 now...

gergoerdi commented 2 years ago

Here's a stack trace:

Debugger entered--Lisp error: (wrong-type-argument sequencep 78)
  length(78)
  (= (length --cl-rest--) 3)
  (if (= (length --cl-rest--) 3) (car-safe (prog1 --cl-rest-- (setq --cl-rest-- (cdr --cl-rest--)))) (signal (quote wrong-number-of-arguments) (list nil (length --cl-rest--))))
  (let* ((--cl-rest-- hole) (name (if (= (length --cl-rest--) 3) (car-safe (prog1 --cl-rest-- (setq --cl-rest-- (cdr --cl-rest--)))) (signal (quote wrong-number-of-arguments) (list nil (length --cl-rest--))))) (premises (car-safe (prog1 --cl-rest-- (setq --cl-rest-- (cdr --cl-rest--))))) (conclusion (car --cl-rest--))) (make-idris2-tree :item name :button (if idris2-enable-elab-prover (list "[E]" (quote help-echo) "Elaborate interactively" (quote action) (function (lambda (_) (interactive) (idris2-prove-hole name t)))) (list "[P]" (quote help-echo) "Open in prover" (quote action) (function (lambda (_) (interactive) (idris2-prove-hole name))))) :highlighting (list (cons 0 (cons (length name) (quote ((...)))))) :print-fn (function idris2-hole-tree-printer) :collapsed-p (not idris2-hole-list-show-expanded) :preserve-properties (quote (idris2-tt-term)) :kids (list (idris2-tree-for-hole-details name premises conclusion))))
  idris2-tree-for-hole(78)
  mapcar(idris2-tree-for-hole "No holes")
  (let ((--dolist-tail-- (mapcar (function idris2-tree-for-hole) hole-info))) (while --dolist-tail-- (let ((tree (car --dolist-tail--))) (idris2-tree-insert tree "") (insert "\n\n") (setq --dolist-tail-- (cdr --dolist-tail--)))))
  (save-current-buffer (set-buffer (idris2-hole-list-buffer)) (setq buffer-read-only nil) (erase-buffer) (idris2-hole-list-mode) (insert (propertize "Holes" (quote face) (quote idris2-info-title-face)) "\n\n") (if idris2-show-help-text (progn (insert "This buffer displays the unsolved holes from the currently-loaded code. ") (insert (concat "Press the " (if idris2-enable-elab-prover "[E]" "[P]") " buttons to solve the holes interactively in the prover.")) (let ((fill-column 80)) (fill-region (point-min) (point-max))) (insert "\n\n"))) (let ((--dolist-tail-- (mapcar (function idris2-tree-for-hole) hole-info))) (while --dolist-tail-- (let ((tree (car --dolist-tail--))) (idris2-tree-insert tree "") (insert "\n\n") (setq --dolist-tail-- (cdr --dolist-tail--))))) (message "Press q to close") (setq buffer-read-only t) (goto-char (point-min)))
  (if (null hole-info) (progn (message "No holes found!") (idris2-hole-list-quit)) (save-current-buffer (set-buffer (idris2-hole-list-buffer)) (setq buffer-read-only nil) (erase-buffer) (idris2-hole-list-mode) (insert (propertize "Holes" (quote face) (quote idris2-info-title-face)) "\n\n") (if idris2-show-help-text (progn (insert "This buffer displays the unsolved holes from the currently-loaded code. ") (insert (concat "Press the " (if idris2-enable-elab-prover "[E]" "[P]") " buttons to solve the holes interactively in the prover.")) (let ((fill-column 80)) (fill-region (point-min) (point-max))) (insert "\n\n"))) (let ((--dolist-tail-- (mapcar (function idris2-tree-for-hole) hole-info))) (while --dolist-tail-- (let ((tree (car --dolist-tail--))) (idris2-tree-insert tree "") (insert "\n\n") (setq --dolist-tail-- (cdr --dolist-tail--))))) (message "Press q to close") (setq buffer-read-only t) (goto-char (point-min))) (display-buffer (idris2-hole-list-buffer)))
  idris2-hole-list-show("No holes")
  idris2-list-holes()
  (progn (idris2-list-holes))
  (if idris2-hole-show-on-load (progn (idris2-list-holes)))
  idris2-list-holes-on-load()
  run-hooks(idris2-load-file-success-hook)
  (closure ((result) (srcdir . "/home/cactus/prog/idris/idris2/bugs/emacs-mode/") (fn . "Hello.idr") (dir-and-fn "/home/cactus/prog/idris/idris2/bugs/emacs-mode/" . "Hello.idr") (set-line . 1) t) nil (idris2-make-clean) (idris2-update-options-cache) (setq idris2-currently-loaded-buffer (current-buffer)) (if (member (quote warnings-tree) idris2-warnings-printing) (progn (idris2-list-compiler-notes))) (run-hooks (quote idris2-load-file-success-hook)) (idris2-update-loaded-region result))()
  funcall((closure ((result) (srcdir . "/home/cactus/prog/idris/idris2/bugs/emacs-mode/") (fn . "Hello.idr") (dir-and-fn "/home/cactus/prog/idris/idris2/bugs/emacs-mode/" . "Hello.idr") (set-line . 1) t) nil (idris2-make-clean) (idris2-update-options-cache) (setq idris2-currently-loaded-buffer (current-buffer)) (if (member (quote warnings-tree) idris2-warnings-printing) (progn (idris2-list-compiler-notes))) (run-hooks (quote idris2-load-file-success-hook)) (idris2-update-loaded-region result)))
  (if (consp result) (let* ((x188 (car result))) (if (eq x188 :highlight-source) (let* ((x189 (cdr result))) (if (consp x189) (let* ((x190 ...) (x191 ...)) (if (null x191) (let ... ...) (idris2-make-clean) (idris2-update-options-cache) (setq idris2-currently-loaded-buffer ...) (if ... ...) (run-hooks ...) (idris2-update-loaded-region result))) (funcall pcase-0))) (funcall pcase-0))) (funcall pcase-0))
  (let* ((pcase-0 (function (lambda nil (idris2-make-clean) (idris2-update-options-cache) (setq idris2-currently-loaded-buffer (current-buffer)) (if (member (quote warnings-tree) idris2-warnings-printing) (progn (idris2-list-compiler-notes))) (run-hooks (quote idris2-load-file-success-hook)) (idris2-update-loaded-region result))))) (if (consp result) (let* ((x188 (car result))) (if (eq x188 :highlight-source) (let* ((x189 (cdr result))) (if (consp x189) (let* (... ...) (if ... ... ... ... ... ... ... ...)) (funcall pcase-0))) (funcall pcase-0))) (funcall pcase-0)))
  (closure ((srcdir . "/home/cactus/prog/idris/idris2/bugs/emacs-mode/") (fn . "Hello.idr") (dir-and-fn "/home/cactus/prog/idris/idris2/bugs/emacs-mode/" . "Hello.idr") (set-line . 1) t) (result) (let* ((pcase-0 (function (lambda nil (idris2-make-clean) (idris2-update-options-cache) (setq idris2-currently-loaded-buffer (current-buffer)) (if (member ... idris2-warnings-printing) (progn ...)) (run-hooks (quote idris2-load-file-success-hook)) (idris2-update-loaded-region result))))) (if (consp result) (let* ((x188 (car result))) (if (eq x188 :highlight-source) (let* ((x189 ...)) (if (consp x189) (let* ... ...) (funcall pcase-0))) (funcall pcase-0))) (funcall pcase-0))))(nil)
  funcall((closure ((srcdir . "/home/cactus/prog/idris/idris2/bugs/emacs-mode/") (fn . "Hello.idr") (dir-and-fn "/home/cactus/prog/idris/idris2/bugs/emacs-mode/" . "Hello.idr") (set-line . 1) t) (result) (let* ((pcase-0 (function (lambda nil (idris2-make-clean) (idris2-update-options-cache) (setq idris2-currently-loaded-buffer ...) (if ... ...) (run-hooks ...) (idris2-update-loaded-region result))))) (if (consp result) (let* ((x188 (car result))) (if (eq x188 :highlight-source) (let* (...) (if ... ... ...)) (funcall pcase-0))) (funcall pcase-0)))) nil)
  (progn (set-buffer buffer) (funcall cont result))
  (if cont (progn (set-buffer buffer) (funcall cont result)))
  (let* ((--cl-rest-- rand-5) (result (if (= (length --cl-rest--) 1) (car --cl-rest--) (signal (quote wrong-number-of-arguments) (list nil (length --cl-rest--)))))) (if cont (progn (set-buffer buffer) (funcall cont result))))
  (cond ((eql op-4 (quote :ok)) (let* ((--cl-rest-- rand-5) (result (if (= (length --cl-rest--) 1) (car --cl-rest--) (signal (quote wrong-number-of-arguments) (list nil ...))))) (if cont (progn (set-buffer buffer) (funcall cont result))))) ((eql op-4 (quote :error)) (let* ((--cl-rest-- rand-5) (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 failure-cont (progn (set-buffer buffer) (funcall failure-cont condition))) (message "Evaluation returned an error: %s." condition)))) (t (error "ELISP destructure-case failed: %S" tmp-6)))
  (let* ((tmp-6 G3) (op-4 (car tmp-6)) (rand-5 (cdr tmp-6))) (cond ((eql op-4 (quote :ok)) (let* ((--cl-rest-- rand-5) (result (if (= ... 1) (car --cl-rest--) (signal ... ...)))) (if cont (progn (set-buffer buffer) (funcall cont result))))) ((eql op-4 (quote :error)) (let* ((--cl-rest-- rand-5) (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 failure-cont (progn (set-buffer buffer) (funcall failure-cont condition))) (message "Evaluation returned an error: %s." condition)))) (t (error "ELISP destructure-case failed: %S" tmp-6))))
  (closure ((failure-cont closure ((srcdir . "/home/cactus/prog/idris/idris2/bugs/emacs-mode/") (fn . "Hello.idr") (dir-and-fn "/home/cactus/prog/idris/idris2/bugs/emacs-mode/" . "Hello.idr") (set-line . 1) t) (_condition) (if (member (quote warnings-tree) idris2-warnings-printing) (progn (idris2-list-compiler-notes) (if idris2-stay-in-current-window-on-compiler-error (display-buffer (idris2-buffer-name :notes)) (pop-to-buffer (idris2-buffer-name :notes)))))) (buffer . #<buffer Hello.idr>) (cont closure ((srcdir . "/home/cactus/prog/idris/idris2/bugs/emacs-mode/") (fn . "Hello.idr") (dir-and-fn "/home/cactus/prog/idris/idris2/bugs/emacs-mode/" . "Hello.idr") (set-line . 1) t) (result) (let* ((pcase-0 (function (lambda nil ... ... ... ... ... ...)))) (if (consp result) (let* ((x188 ...)) (if (eq x188 :highlight-source) (let* ... ...) (funcall pcase-0))) (funcall pcase-0)))) (failure-cont closure ((srcdir . "/home/cactus/prog/idris/idris2/bugs/emacs-mode/") (fn . "Hello.idr") (dir-and-fn "/home/cactus/prog/idris/idris2/bugs/emacs-mode/" . "Hello.idr") (set-line . 1) t) (_condition) (if (member (quote warnings-tree) idris2-warnings-printing) (progn (idris2-list-compiler-notes) (if idris2-stay-in-current-window-on-compiler-error (display-buffer (idris2-buffer-name :notes)) (pop-to-buffer (idris2-buffer-name :notes)))))) (cont closure ((srcdir . "/home/cactus/prog/idris/idris2/bugs/emacs-mode/") (fn . "Hello.idr") (dir-and-fn "/home/cactus/prog/idris/idris2/bugs/emacs-mode/" . "Hello.idr") (set-line . 1) t) (result) (let* ((pcase-0 (function (lambda nil ... ... ... ... ... ...)))) (if (consp result) (let* ((x188 ...)) (if (eq x188 :highlight-source) (let* ... ...) (funcall pcase-0))) (funcall pcase-0)))) (sexp :load-file "Hello.idr") idris2-event-hooks t) (G3) (let* ((tmp-6 G3) (op-4 (car tmp-6)) (rand-5 (cdr tmp-6))) (cond ((eql op-4 (quote :ok)) (let* ((--cl-rest-- rand-5) (result (if ... ... ...))) (if cont (progn (set-buffer buffer) (funcall cont result))))) ((eql op-4 (quote :error)) (let* ((--cl-rest-- rand-5) (condition (if --cl-rest-- ... ...)) (_spans (car-safe ...))) (progn (if --cl-rest-- (signal ... ...)) (if failure-cont (progn ... ...)) (message "Evaluation returned an error: %s." condition)))) (t (error "ELISP destructure-case failed: %S" tmp-6)))))((:ok nil))
  funcall((closure ((failure-cont closure ((srcdir . "/home/cactus/prog/idris/idris2/bugs/emacs-mode/") (fn . "Hello.idr") (dir-and-fn "/home/cactus/prog/idris/idris2/bugs/emacs-mode/" . "Hello.idr") (set-line . 1) t) (_condition) (if (member (quote warnings-tree) idris2-warnings-printing) (progn (idris2-list-compiler-notes) (if idris2-stay-in-current-window-on-compiler-error (display-buffer ...) (pop-to-buffer ...))))) (buffer . #<buffer Hello.idr>) (cont closure ((srcdir . "/home/cactus/prog/idris/idris2/bugs/emacs-mode/") (fn . "Hello.idr") (dir-and-fn "/home/cactus/prog/idris/idris2/bugs/emacs-mode/" . "Hello.idr") (set-line . 1) t) (result) (let* ((pcase-0 (function ...))) (if (consp result) (let* (...) (if ... ... ...)) (funcall pcase-0)))) (failure-cont closure ((srcdir . "/home/cactus/prog/idris/idris2/bugs/emacs-mode/") (fn . "Hello.idr") (dir-and-fn "/home/cactus/prog/idris/idris2/bugs/emacs-mode/" . "Hello.idr") (set-line . 1) t) (_condition) (if (member (quote warnings-tree) idris2-warnings-printing) (progn (idris2-list-compiler-notes) (if idris2-stay-in-current-window-on-compiler-error (display-buffer ...) (pop-to-buffer ...))))) (cont closure ((srcdir . "/home/cactus/prog/idris/idris2/bugs/emacs-mode/") (fn . "Hello.idr") (dir-and-fn "/home/cactus/prog/idris/idris2/bugs/emacs-mode/" . "Hello.idr") (set-line . 1) t) (result) (let* ((pcase-0 (function ...))) (if (consp result) (let* (...) (if ... ... ...)) (funcall pcase-0)))) (sexp :load-file "Hello.idr") idris2-event-hooks t) (G3) (let* ((tmp-6 G3) (op-4 (car tmp-6)) (rand-5 (cdr tmp-6))) (cond ((eql op-4 (quote :ok)) (let* ((--cl-rest-- rand-5) (result ...)) (if cont (progn ... ...)))) ((eql op-4 (quote :error)) (let* ((--cl-rest-- rand-5) (condition ...) (_spans ...)) (progn (if --cl-rest-- ...) (if failure-cont ...) (message "Evaluation returned an error: %s." condition)))) (t (error "ELISP destructure-case failed: %S" tmp-6))))) (:ok nil))
  (cond (rec (setq idris2-rex-continuations (remove rec idris2-rex-continuations)) (funcall (car (cdr rec)) value)) (t (error "Unexpected reply: %S %S" id value)))
  (let ((rec (assq id idris2-rex-continuations))) (cond (rec (setq idris2-rex-continuations (remove rec idris2-rex-continuations)) (funcall (car (cdr rec)) value)) (t (error "Unexpected reply: %S %S" id value))))
  (let* ((--cl-rest-- rand-1) (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 idris2-rex-continuations))) (cond (rec (setq idris2-rex-continuations (remove rec idris2-rex-continuations)) (funcall (car (cdr rec)) value)) (t (error "Unexpected reply: %S %S" id value)))))
  (cond ((eql op-0 (quote :emacs-rex)) (let* ((--cl-rest-- rand-1) (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 idris2-continuation-counter ...))) (idris2-send (list form id) process) (setq idris2-rex-continuations (cons (if output-continuation ... ...) idris2-rex-continuations)))))) ((eql op-0 (quote :output)) (let* ((--cl-rest-- rand-1) (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 idris2-rex-continuations))) (if (and rec (nth 2 rec)) (progn (funcall (nth 2 rec) value)))))) ((eql op-0 (quote :return)) (let* ((--cl-rest-- rand-1) (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 idris2-rex-continuations))) (cond (rec (setq idris2-rex-continuations (remove rec idris2-rex-continuations)) (funcall (car ...) value)) (t (error "Unexpected reply: %S %S" id value)))))) (t (error "ELISP destructure-case failed: %S" tmp-2)))
  (let* ((tmp-2 event) (op-0 (car tmp-2)) (rand-1 (cdr tmp-2))) (cond ((eql op-0 (quote :emacs-rex)) (let* ((--cl-rest-- rand-1) (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 ...)) (idris2-send (list form id) process) (setq idris2-rex-continuations (cons ... idris2-rex-continuations)))))) ((eql op-0 (quote :output)) (let* ((--cl-rest-- rand-1) (value (if (= ... 2) (car-safe ...) (signal ... ...))) (id (car --cl-rest--))) (let ((rec (assq id idris2-rex-continuations))) (if (and rec (nth 2 rec)) (progn (funcall ... value)))))) ((eql op-0 (quote :return)) (let* ((--cl-rest-- rand-1) (value (if (= ... 2) (car-safe ...) (signal ... ...))) (id (car --cl-rest--))) (let ((rec (assq id idris2-rex-continuations))) (cond (rec (setq idris2-rex-continuations ...) (funcall ... value)) (t (error "Unexpected reply: %S %S" id value)))))) (t (error "ELISP destructure-case failed: %S" tmp-2))))
  (or (run-hook-with-args-until-success (quote idris2-event-hooks) event) (let* ((tmp-2 event) (op-0 (car tmp-2)) (rand-1 (cdr tmp-2))) (cond ((eql op-0 (quote :emacs-rex)) (let* ((--cl-rest-- rand-1) (form (if ... ... ...)) (continuation (car-safe ...)) (output-continuation (car-safe ...))) (progn (if --cl-rest-- (signal ... ...)) (let (...) (idris2-send ... process) (setq idris2-rex-continuations ...))))) ((eql op-0 (quote :output)) (let* ((--cl-rest-- rand-1) (value (if ... ... ...)) (id (car --cl-rest--))) (let ((rec ...)) (if (and rec ...) (progn ...))))) ((eql op-0 (quote :return)) (let* ((--cl-rest-- rand-1) (value (if ... ... ...)) (id (car --cl-rest--))) (let ((rec ...)) (cond (rec ... ...) (t ...))))) (t (error "ELISP destructure-case failed: %S" tmp-2)))))
  idris2-dispatch-event((:return (:ok nil) 14) #<process Idris2 IDE support>)
  (save-current-buffer (idris2-dispatch-event event process))
  (unwind-protect (save-current-buffer (idris2-dispatch-event event process)))
  (let ((event (idris2-receive))) (idris2-event-log event nil) (unwind-protect (save-current-buffer (idris2-dispatch-event event process))))
  (while (idris2-have-input-p) (let ((event (idris2-receive))) (idris2-event-log event nil) (unwind-protect (save-current-buffer (idris2-dispatch-event event process)))))
  (save-current-buffer (set-buffer (process-buffer process)) (while (idris2-have-input-p) (let ((event (idris2-receive))) (idris2-event-log event nil) (unwind-protect (save-current-buffer (idris2-dispatch-event event process))))))
  idris2-connection-available-input(#<process Idris2 IDE support>)
  idris2-output-filter(#<process Idris2 IDE support> "0000cc(:output (:ok (:highlight-source ((((:filename \"Hello.idr\") (:start 5 8) (:end 5 9)) ((:name \"IO\") (:namespace \"PrimIO\") (:decor :type) (:implicit :False) (:key \"\") (:doc-overview \"\") (:type \"\")))))) 14)\n0000d1(:output (:ok (:highlight-source ((((:filename \"Hello.idr\") (:start 5 11) (:end 5 12)) ((:name \"Unit\") (:namespace \"Builtin\") (:decor :type) (:implicit :False) (:key \"\") (:doc-overview \"\") (:type \"\")))))) 14)\n0000d1(:output (:ok (:highlight-source ((((:filename \"Hello.idr\") (:start 6 1) (:end 6 4)) ((:name \"main\") (:namespace \"Hello\") (:decor :function) (:implicit :False) (:key \"\") (:doc-overview \"\") (:type \"\")))))) 14)\n000071(:output (:ok (:highlight-source ((((:filename \"Hello.idr\") (:start 6 6) (:end 6 6)) ((:decor :keyword)))))) 14)\n0000db(:output (:ok (:highlight-source ((((:filename \"Hello.idr\") (:start 6 8) (:end 6 15)) ((:name \"putStrLn\") (:namespace \"Prelude.IO\") (:decor :function) (:implicit :False) (:key \"\") (:doc-overview \"\") (:type \"\")))))) 14)\n000070(:output (:ok (:highlight-source ((((:filename \"Hello.idr\") (:start 6 17) (:end 6 30)) ((:decor :data)))))) 14)\n000016(:return (:ok ()) 14)\n")

gergoerdi commented 2 years ago

I think the meaningful part is this:

  idris2-tree-for-hole(78)
  mapcar(idris2-tree-for-hole "No holes")
  idris2-hole-list-show("No holes")
  idris2-list-holes()

The definition of idris2-list-holes is:

(defun idris2-list-holes ()
  "Get a list of currently-open holes"
  (interactive)
  (idris2-hole-list-show (car (idris2-eval '(:metavariables 80)))))

So it seems (car (idris2-eval '(:metavariables 80))) returns the string "No holes" instead of a list of holes as expected by idris2-hole-list-show.

gallais commented 2 years ago

It used to be that :m led to an error [1] which I have fixed by changing the way we respond to this query for metavariables: https://github.com/idris-lang/Idris2/pull/1934

Was this using the same query but somehow expecting a different format as a response?

[1] From the discord:

Am I the only one getting an error when I input :m in the emacs REPL?

error in process filter: progn: Wrong type argument: char-or-string-p, (("AlmostFull.aslgj" ((" 0 x" "Type" nil) (" 0 rel" "x -> x -> Type" nil) (" f" "x -> WFT x" nil) (" sec" "(a : x) -> SecureBy (\i => \j => Either (rel i j) (rel a i)) (f a)" nil) (" y" "y" nil)) ("(a : Either x y) -> SecureBy (\i => \j => Eit (...)

gergoerdi commented 2 years ago

I'm running Idris 0.5.1 so it should already contain https://github.com/idris-lang/Idris2/pull/1934

The response from Idris seems to be:

(:return (:ok No holes nil) 9)

or

(:return (:ok 1 hole: Hello.main : IO () ((21 2 ((:decor :type))))) 13)

gergoerdi commented 2 years ago

If I type :m into the REPL in Emacs, I don't get an error, I get the following output:

λΠ> :m
1 hole: Hello.main : IO ()

gallais commented 2 years ago

Yeah my point being that 2 different mechanisms are using this IDE protocol query (:m from the REPL and auto-display of holes after loading) but they seem to be expecting the answer to be in different formats.

So when I fixed the answer for :m, it may have broken it for the other thing?

gergoerdi commented 2 years ago

If I revert https://github.com/idris-lang/Idris2/commit/87c1cb697f93d4c2b42a145aa25af6c322a9a391 it works!

gallais commented 2 years ago

~~I have had a look at idris2-mode and can confirm it's relying on the same :metavariables command as the REPL but interpreting its output differently. This is 100% incompatible.

We could either modify idris2-repl to make it handle the metavariables command in the REPL in an ad-hoc way to make it work just like the show holes functionality that kicks in after a load.

Alternatively (my preferred solution), we could add a :list-metavariables command to the IDE protocol that would have the previous behaviour. Then we can patch idris2-commands to call this new command instead of :metavariables.

@jfdm Not sure how to handle this in idris-mode that wants to be compatible across versions of the compiler.~~

Edit: Nevermind! The emacs mode sends the REPL commands over as :interpret ... so we already have 2 distinct commands: :metavariables vs. :interpret :m It seems that the current implementations of :metavariables was to simply piggy-back on :interpret :m which is plainly wrong. This should be a fairly easy (and hopefully backwards compatible) fix now!

gallais commented 2 years ago

@gergoerdi Can you please test & confirm whether the following PR fixes the issue? https://github.com/idris-lang/Idris2/pull/1973

gergoerdi commented 2 years ago

I can confirm with that PR merged, idris2-mode works for me.

gallais commented 2 years ago

Thanks for the bug report, the investigation, and the testing!

ju-sh commented 1 year ago

Had this problem with an older idris-mode. Updated the package and it works. Thanks.

idris-hackers / idris-mode

error in process filter: Wrong type argument: sequencep, 78 #542