<div dir="ltr">One possibility might be to add support for local 'libraries' files. That way you could distribute<div>your project together with a special libraries file for the funky dependencies, without cluttering</div><div>the agda-lib file with explicit paths.</div><div><br></div><div>/ Ulf</div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Nov 10, 2017 at 4:51 PM, Frederik Hanghøj Iversen <span dir="ltr"><<a href="mailto:fhi.1990@gmail.com" target="_blank">fhi.1990@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><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" target="_blank">http://agda.readthedocs.<wbr>io/en/v2.5.2/tools/package-<wbr>system.html?highlight=agda-<wbr>lib#installing-libraries</a><span class="HOEnZb"><font color="#888888"><br></font></span></div></div><span class="HOEnZb"><font color="#888888"><div><div><div><br></div>-- <br><div class="m_-7665249937735035722gmail_signature"><div>Regards</div><div><i>Frederik Hanghøj Iversen</i></div></div>
</div></div></font></span></div>
<br>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div></div>