Nested Packages Can't Find Their Parents

[rvs314]

When opening a nested package (a package defined within another package), idris-mode can't seem to find the outer package, as idris itself can. When trying to run test code from the REPL, I get the following error:

Evaluation returned an error: Failed to resolve the dependencies for frombus-test:
  required frombus any but no matching version is installed

The complete file tree looks like this:

.
├── frombus.ipkg
├── pack.toml
├── src
│   └── Frombus.idr
└── test
    ├── src
    │   └── Main.idr
    └── test.ipkg

I happened to use pack to generate this project scaffold, but I don't think its the cause of the issue.

Here are the contents of the relevant files:

[custom.all.frombus]
type = "local"
path = "."
ipkg = "frombus.ipkg"
test = "test/test.ipkg"

[custom.all.frombus-test]
type = "local"
path = "test"
ipkg = "test.ipkg"

-- frombus.ipkg
package frombus
version = 0.1.0
modules = Frombus
sourcedir = "src"

-- src/Frombus.idr
module Frombus

test : String
test = "Hello from Idris2!"

-- test/test.ipkg
package frombus-test
version = 0.1.0
depends = frombus
main = Main
executable = "frombus-test"
sourcedir = "src"

-- test/src/Main.idr
module Main

main : IO ()
main = putStrLn "Test successful!"

When I open src/Frombus.idr, everything works fine. However, when I open test/src/Main.idr and execute idris-load-file, the error is reported.

I'm not totally sure, but I think it's a bug in the emacs major mode rather than idris. I can build and run the tests (either by hand or through pack), can find frombus as an available package when I run idris2 --list-packages, and can run idris2 --repl test/test.ipkg without issue.

[FFFluoride]

I get something similar with my setup.

ipkg file:

package display

-- Display
-- by FFFluoride

opts = ""
sourcedir = "src"
modules = Display.Old
    , Display.New
    , Main

My source tree looks like this:

Everything builds when I load the REPL:

But I get weird error marks:

edit: Everything works except the highlighting so it isn't a huge issue or anything

[keram]

We are getting closer to fix this although there is still some weird behaviour that I don't understand yet. Cold start of Idris2 by loading test/src/Main.idr works correctly as at the beginning we also set the correct working directory. What puzzles me is that after making the Main.idr file dirty and trying to load it again we get the error Source file "Main.idr" is not in the source directory "/home/m/work/idris/frombus/test/src. But actually seems like Idris itself changed the working directory to /home/m/work/idris/frombus/test This creates mismatch between working directory of the idris-mode stored in idris-process-current-working-directory and Idris working directory. Here are relevant logs for later investigation:

23:39:12 -> ((:interpret ":cd \"/home/m/work/idris/frombus/test/src\"")
 112)
23:39:12 <- (:return
 (:ok "Current working directory is \"/home/m/work/idris/frombus/test/src\"")
 112)
23:39:12 -> ((:load-file "Main.idr")
 113)
23:39:12 <- (:write-string "1/1: Building Main (src/Main.idr)" 113)
23:39:20 -> ((:interpret ":cwd")
 116)
23:39:20 <- (:return
 (:ok "Current working directory is \"/home/m/work/idris/frombus/test\"")
 116)
23:39:36 -> ((:load-file "Main.idr")
 117)
23:39:36 <- (:return
 (:error "Error: Source file \"Main.idr\" is not in the source directory \"/home/m/work/idris/frombus/test/src\"")
 117)