<div dir="ltr">I'm reading up on library management in Agda[1]. From what I gather it is not possible to install a certain library to be used in a specific project. Is this correct?<div><br></div><div>What I'm hoping for is the possibility to put something like the following in my .agda-lib file:</div><div><br></div><div><div>name: my-project</div><div>depend:</div><div>  funky-dep</div><div>include:</div><div>  src</div><div>libs:</div><div>  path-to-funky-dep</div><div><br></div><div>Where funky-dep is some dependencies I don't want to make available to all agda projects on my machine, but rather just for the purpose of developing "my-project".</div><div><br></div><div>Is this is possible it would also make it a lot easier to share code with other people. That way you can package your code along with all it's dependencies and you don't need the recipient to make changes to their global configuration.</div><div><br></div><div>The way I understand it, at the moment it's only possible to add path-to-funky-dep to $AGDA_DIR/libraries (as per [1]).</div><div><br></div><div>[1]: <a href="http://agda.readthedocs.io/en/v2.5.2/tools/package-system.html?highlight=agda-lib#installing-libraries">http://agda.readthedocs.io/en/v2.5.2/tools/package-system.html?highlight=agda-lib#installing-libraries</a><br></div></div><div><div><div><br></div>-- <br><div class="gmail_signature"><div>Regards</div><div><i>Frederik Hanghøj Iversen</i></div></div>
</div></div></div>