Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
keram opened this issue Jun 13, 2024 · 0 comments

Comments

@keram
Copy link
Contributor

keram commented Jun 13, 2024

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 idris-hackers/idris-mode#624

keram added a commit to keram/idris-mode that referenced this issue Jul 8, 2024
"source dir" and "relative file path" or
"work dir" and "relative file path" when idris protocol version
is greater than 1.

Why:
In Idris2 the files are loaded relative to work directory
which is a directory containing an ".ipkg" file.

Relates to:
idris-lang/Idris2#3310
idris-hackers#627
keram added a commit to keram/idris-mode that referenced this issue Jul 8, 2024
"source dir" and "relative file path" or
"work dir" and "relative file path" when idris protocol version
is greater than 1.

Why:
In Idris2 the files are loaded relative to work directory
which is a directory containing an ".ipkg" file.

Relates to:
idris-lang/Idris2#3310
idris-hackers#627
keram added a commit to keram/idris-mode that referenced this issue Jul 13, 2024
"source dir" and "relative file path" or
"work dir" and "relative file path" when idris protocol version
is greater than 1.

Why:
In Idris2 the files are loaded relative to work directory
which is a directory containing an ".ipkg" file.

Relates to:
idris-lang/Idris2#3310
idris-hackers#627
keram added a commit to keram/idris-mode that referenced this issue Jul 15, 2024
"source dir" and "relative file path" or
"work dir" and "relative file path" when idris protocol version
is greater than 1.

Why:
In Idris2 the files are loaded relative to work directory
which is a directory containing an ".ipkg" file.

Relates to:
idris-lang/Idris2#3310
idris-hackers#627
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant