<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
At some point I was looking for similar functionality, but am very
content now using git sub-modules for tracking<br>
specific versions of "funky" dependencies in the project repository.<br>
<br>
Assuming you are using git and that your dependencies are tracked in
git, this makes it very easy to pull in the <br>
correct versions and instead of using the 'depend' key in your
.agda-lib file, you use the project-root relative<br>
include paths.<br>
<br>
For an example see the following .agda-lib file and makefile in this
repository [1].<br>
The makefile is set up to do all the work for you when you run
`make`.<br>
<br>
[1]: <a class="moz-txt-link-freetext" href="https://github.com/metaborg/mj.agda/">https://github.com/metaborg/mj.agda/</a><br>
<br>
Cheers,<br>
<br>
<br>
Arjen<br>
<br>
<div class="moz-cite-prefix">On 11/10/2017 07:24 PM, Ulf Norell
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAJjNqYGeV8T-tesGkV7nbUf6SGHPqA+qyPfWm-KBB3sVU6gaoQ@mail.gmail.com">
<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"
moz-do-not-send="true">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" moz-do-not-send="true">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"
moz-do-not-send="true">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda"
rel="noreferrer" target="_blank" moz-do-not-send="true">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br>
</blockquote>
</div>
<br>
</div>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</body>
</html>