We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
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
depends
setup a project like this:
├── depends │ └── dep-0 │ ├── dep.ipkg │ └── src │ └── Dep.idr ├── main.ipkg └── src └── Main.idr
With main.ipkg containing:
main.ipkg
package main depends = dep sourcedir = "src"
and dep.ipkg containing:
dep.ipkg
package dep version = 0 modules = Dep sourcedir = "src"
Main.idr:
module Main import Dep main : IO () main = putStrLn str
Dep.idr:
module Dep str : String str = "hello"
Compiling main with idris2 --build main.ipkg should work.
idris2 --build main.ipkg
Uncaught error: "Depends/depends/dep-0/dep.ipkg":4:11--6:1:Dep not found
If the dependency is instead installed globally with --install and the depends folder removed, the project works just fine
--install
The text was updated successfully, but these errors were encountered:
No branches or pull requests
Steps to Reproduce
setup a project like this:
With
main.ipkg
containing:and
dep.ipkg
containing:Main.idr:
Dep.idr:
Expected Behavior
Compiling main with
idris2 --build main.ipkg
should work.Observed Behavior
If the dependency is instead installed globally with
--install
and thedepends
folder removed, the project works just fineThe text was updated successfully, but these errors were encountered: