You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Ubuntu 22.04 LTS
GNU Emacs 27.1
Idris version 0.5.1-68a144bf1
If I already have idris2 --ide-mode-socket running somewhere, running it again produces an error message:
$ idris2 --ide-mode-socket &
38398
$ idris2 --ide-mode-socket
Failed to bind socket with error: 98
If, while I have idris2 --ide-mode-socket running elsewhere, I try idris2-run in Emacs, I see this error:
Warning from Idris2: Failed to bind socket with error:
error in process filter: open-network-stream: make client process failed: Connection refused, :name, Idris2 IDE support, :buffer, *idris2-connection*, :host, 127.0.0.1, :service, 98, :nowait, nil, :tls-parameters, nil
error in process filter: make client process failed: Connection refused, :name, Idris2 IDE support, :buffer, *idris2-connection*, :host, 127.0.0.1, :service, 98, :nowait, nil, :tls-parameters, nil
Idris2 disconnected: exited abnormally with code 1
This is a bit strange. What seems to be happening is that idris2-process-filter has a bug or misfeature:
(defunidris2-process-filter (string)
"Accept output from the process"
(if idris2-connection
string
;; Idris2 sometimes prints a warning prior to the port number, which causes;; `string-match' to return 0
(cl-flet ((idris2-warn (msg)
(unless (or (null msg) (string-blank-p msg))
(message"Warning from Idris2: %s" msg))))
(if (not (string-match idris2-process-port-output-regexp string))
(idris2-warn string)
(idris2-warn (match-string1 string))
(idris2-connect (string-to-number (match-string2 string))))
"")))
Here, string gets bound to "Failed to bind socket with error: 98\n". Then string-matchsucceeds (returning 0) because there is indeed a number in this string and idris2-process-port-output-regexp is not start-/end-anchored. So we take the second branch, warn about the part of the string before the number, and interpret 98 as a port number. Unfortunately, it isn't.
The simplest way to fix this would be to anchor idris2-process-port-output-regexp (add ^ to beginning and $ to the end). Unfortunately, the way the code is written suggests there's some case where idris2 --ide-mode-socket produces a warning followed by a genuine port number. I'm not sure what this case is, so I don't know the best way to distinguish between that case and this one.
I think I ran into this problem because I had tried loading a file with idris-mode, which had managed to start an idris2 process but had some unrelated problem, so I tried installing idris2-mode and when I tried to load the file with idris2-mode, the old process was still around.
It also seems unfortunate that idris2 --ide-mode-socket fails if a copy is already running, I'll try to report that upstream.
The text was updated successfully, but these errors were encountered:
Ubuntu 22.04 LTS
GNU Emacs 27.1
Idris version 0.5.1-68a144bf1
If I already have
idris2 --ide-mode-socket
running somewhere, running it again produces an error message:If, while I have
idris2 --ide-mode-socket
running elsewhere, I tryidris2-run
in Emacs, I see this error:This is a bit strange. What seems to be happening is that
idris2-process-filter
has a bug or misfeature:Here,
string
gets bound to"Failed to bind socket with error: 98\n"
. Thenstring-match
succeeds (returning 0) because there is indeed a number in this string andidris2-process-port-output-regexp
is not start-/end-anchored. So we take the second branch, warn about the part of the string before the number, and interpret98
as a port number. Unfortunately, it isn't.The simplest way to fix this would be to anchor
idris2-process-port-output-regexp
(add^
to beginning and$
to the end). Unfortunately, the way the code is written suggests there's some case whereidris2 --ide-mode-socket
produces a warning followed by a genuine port number. I'm not sure what this case is, so I don't know the best way to distinguish between that case and this one.I think I ran into this problem because I had tried loading a file with
idris-mode
, which had managed to start an idris2 process but had some unrelated problem, so I tried installing idris2-mode and when I tried to load the file withidris2-mode
, the old process was still around.It also seems unfortunate that
idris2 --ide-mode-socket
fails if a copy is already running, I'll try to report that upstream.The text was updated successfully, but these errors were encountered: