[Agda] Finer-grained library control in Agda

[Ulf Norell]

I'm not sure I understand your problem exactly, but note that registering a
package in `~/.agda/libraries` only makes it available as a possible
dependency. As long as the library name doesn't clash with other libraries
and you don't add it to `~/.agda/defaults` it will not interfere with other
libraries. In your case it should be enough to rename the modified version
of the standard library (or add a special version number [1]).

/ Ulf

[1]
http://agda.readthedocs.io/en/latest/tools/package-system.html#version-numbers

On Fri, Feb 16, 2018 at 9:59 AM, Frederik Hanghøj Iversen <
fhi.1990 at gmail.com> wrote:

> Can I depend on a package only locally?
>
> I know I can put a package in `~/.agda/libraries` and thus make it
> available globally on my system.
>
> 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.
>
> 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.
>
> --
> Regards
> *Frederik Hanghøj Iversen*
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180216/1750c786/attachment.html>