Idris2 icon indicating copy to clipboard operation
Idris2 copied to clipboard

Loading file in ide-mode changes working directory and causes errors on later actions

Open keram opened this issue 1 year ago • 0 comments

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 :cd command.
  • No error returned when loading file second time
  • The error should mention the same source directory as output of :cwd command

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

keram avatar Jun 13 '24 22:06 keram