Idris2
Idris2 copied to clipboard
Loading file in ide-mode changes working directory and causes errors on later actions
After loading a file the Idris2 changes working directory to one level higher and same time keeps reference to the original working directory leading to error Source file X is not in the source directory Y
Reproduced on Idris2 build from main Idris 2, version 0.7.0-055568be2 build on linux with chez scheme.
Steps to Reproduce
Please see the steps below reproduced on Idris2 repository itself.
# <- marks output from Idris, # -> marks input by user
~/sources/Idris2/src$ rlwrap idris2 --ide-mode
# <-
(:protocol-version 2 1)
# ->
((:interpret ":cwd") 26)
# <-
(:return (:ok "Current working directory is \"/x/sources/Idris2/src\"") 26)
# ->
((:load-file "Idris/Main.idr") 64)
# <-
(:output (:ok (:highlight-source ((((:filename "src/Idris/Main.idr") (:start 0 0) (:end 0 6)) ((:decor :keyword)))))) 64)
..
(:output (:ok (:highlight-source ((((:filename "src/Idris/Main.idr") (:start 6 24) (:end 6 26)) ((:name "Nil") (:namespace "Prelude.Basics") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 64)
(:return (:ok ()) 64)
# ->
((:interpret ":cwd") 26)
# <-
(:return (:ok "Current working directory is \"/x/sources/Idris2\"") 26)
# ->
((:load-file "Idris/Main.idr") 64)
# <-
(:return (:error "Error: Source file \"Idris/Main.idr\" is not in the source directory \"/x/sources/Idris2/src\"") 64)
Expected Behavior
- The working directory stay's unchanged unless user invokes
:cdcommand. - No error returned when loading file second time
- The error should mention the same source directory as output of
:cwdcommand
Observed Behavior
- working directory changed behind the scenes
- loading files fails and erroris returned
This is very likely related also to reported issue in idris-mode https://github.com/idris-hackers/idris-mode/issues/624