idris-lang / Idris2

A purely functional programming language with first class types
https://idris-lang.org/
Other
2.53k stars 380 forks source link

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

Open keram opened 5 months ago

keram commented 5 months ago

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

Observed Behavior

This is very likely related also to reported issue in idris-mode https://github.com/idris-hackers/idris-mode/issues/624