[x] I have checked that there is no existing PR/issue about my proposal.
Summary
Sometimes there are two or more ipkg files in a directory. --find-ipkg only load the first file it finds, but what if you want to use another ipkg file?
Technical implementation
Add a new option (maybe --ipkg) or make -p load package from source if "package name" ends in .ipkg.
Alternatives considered
add current directory to library path
Additional Remarks
I think a rewrite for package management in necessary. Currently, idris2 just find package in a centralized location. There isn't any way to use a library in development (like pip install -e .).
There are way too many stuff named findipkg in source code.
FindIPKG in src/Idris/CommandLine.idr
Core.Option: findipkg
Summary
Sometimes there are two or more ipkg files in a directory.
--find-ipkg
only load the first file it finds, but what if you want to use another ipkg file?Technical implementation
Add a new option (maybe
--ipkg
) or make-p
load package from source if "package name" ends in.ipkg
.Alternatives considered
Additional Remarks
I think a rewrite for package management in necessary. Currently, idris2 just find package in a centralized location. There isn't any way to use a library in development (like
pip install -e .
).There are way too many stuff named
findipkg
in source code.FindIPKG
insrc/Idris/CommandLine.idr
Core.Option:findipkg