Historically I have hard coded assumptions about where Idris will install a package when idris2 --install is called. This works, but it's fragile, inconvenient, and far from obvious.
See, for example, this snippet from one of my C support library Makefiles:
While I was adding --dump-installdir anyway, I also used it in the existing Nix buildIdris function to better support a "Pack-ism" where C support libraries are installed to the ./lib folder and Pack takes care of the rest. Now buildIdris also takes care of the rest.
Should this change go in the CHANGELOG?
[x] If this is a fix, user-facing change, a compiler change, or a new paper
implementation, I have updated CHANGELOG_NEXT.md (and potentially also
CONTRIBUTORS.md).
Description
Historically I have hard coded assumptions about where Idris will install a package when
idris2 --install
is called. This works, but it's fragile, inconvenient, and far from obvious.See, for example, this snippet from one of my C support library Makefiles:
This PR introduces
idris2 --dump-installdir
which could make the above Makefile snippet much more reasonable:While I was adding
--dump-installdir
anyway, I also used it in the existing NixbuildIdris
function to better support a "Pack-ism" where C support libraries are installed to the./lib
folder and Pack takes care of the rest. NowbuildIdris
also takes care of the rest.Should this change go in the CHANGELOG?
CHANGELOG_NEXT.md
(and potentially alsoCONTRIBUTORS.md
).