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

Nested Packages Can't Find Their Parents #624

Open
rvs314 opened this issue Feb 20, 2024 · 2 comments
Open

Nested Packages Can't Find Their Parents #624

rvs314 opened this issue Feb 20, 2024 · 2 comments

Comments

@rvs314
Copy link

rvs314 commented Feb 20, 2024

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
Copy link

FFFluoride commented May 5, 2024

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:
Screenshot from 2024-05-05 09-57-49

Everything builds when I load the REPL:
Screenshot from 2024-05-05 10-00-04

But I get weird error marks:
Screenshot from 2024-05-05 10-01-14

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

keram added a commit to keram/idris-mode that referenced this issue Jun 8, 2024
update the regexp to include also double quotes.

Why:
In Idris2 the sourcedir option has double quotes.

Relates to:
idris-hackers#624
@keram
Copy link
Contributor

keram commented Jun 10, 2024

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)

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

3 participants