<div dir="ltr"><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">Yeah I had been thinking of that. Actually I think I did go down that road previously but ran into some other annoying snag.</span><div style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration-style:initial;text-decoration-color:initial"><br></div><div style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration-style:initial;text-decoration-color:initial">This is really quite hampering for library writers. I have a few ideas that I would love to implement, but I'm a bit hesitant to start working on it since I think it might be require quite a big refactor of Agda.</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Feb 16, 2018 at 10:08 AM, a.j.rouvoet <span dir="ltr"><<a href="mailto:a.j.rouvoet@gmail.com" target="_blank">a.j.rouvoet@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 text="#000000" bgcolor="#FFFFFF">
<p>The indirection via a global libraries file is a limitation of
the Agda library system I also run into now and then.<br>
My best approximation of what you are asking for is to have
project-local copies of the (right versions of) libraries I depend
on.<br>
E.g. via git submodules. And instead of adding them in the
`depends:` section, you add them to the `include:` section of your
agda-lib file.<br>
<br>
An example project that uses this setup can be found here:
<a class="m_-898721615309747073moz-txt-link-freetext" href="https://github.com/metaborg/mj.agda" target="_blank">https://github.com/metaborg/<wbr>mj.agda</a><br>
Check the makefile and the .agda-lib file <br>
<br>
Arjen<br>
</p><div><div class="h5">
<br>
<div class="m_-898721615309747073moz-cite-prefix">On 02/16/2018 09:59 AM, Frederik
Hanghøj Iversen wrote:<br>
</div>
</div></div><blockquote type="cite"><div><div class="h5">
<div dir="ltr">Can I depend on a package only locally?
<div><br>
</div>
<div>I know I can put a package in `~/.agda/libraries` and thus
make it available globally on my system.</div>
<div><br>
</div>
<div>What I really need is a way for a library to ship with it's
own dependencies. So that I can e.g. use git-submodules to
explicitly list dependencies.</div>
<div><br>
</div>
<div>The problem I have is that I'm working on a library that
explicitly does not want to depend on the standard library
(for reasons I guess) - but I also need to use this library in
another library that depends on this library *and* the
standard library - but it would make my life a *lot easier* if
we agreed on the definition of e..g Sigma. So I want to depend
on a modified version of the library. But if I have two
versions lying around in my system I can work on the
dependency as all module names are suddenly ambiguous. And if
I don't register the dependency globally I cannot use it in
the dependent package.</div>
<div>
<div><br>
</div>
-- <br>
<div class="m_-898721615309747073gmail_signature" data-smartmail="gmail_signature">
<div>Regards</div>
<div><i>Frederik Hanghøj Iversen</i></div>
</div>
</div>
</div>
<br>
<fieldset class="m_-898721615309747073mimeAttachmentHeader"></fieldset>
<br>
</div></div><pre>______________________________<wbr>_________________
Agda mailing list
<a class="m_-898721615309747073moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a>
<a class="m_-898721615309747073moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</div>
</blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="gmail_signature" data-smartmail="gmail_signature"><div>Regards</div><div><i>Frederik Hanghøj Iversen</i></div></div>
</div>