[Agda] Finer-grained library control in Agda

[Frederik Hanghøj Iversen]

Yeah I had been thinking of that. Actually I think I did go down that road
previously but ran into some other annoying snag.

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.

On Fri, Feb 16, 2018 at 10:08 AM, a.j.rouvoet <a.j.rouvoet at gmail.com> wrote:

> The indirection via a global libraries file is a limitation of the Agda
> library system I also run into now and then.
> My best approximation of what you are asking for is to have project-local
> copies of the (right versions of) libraries I depend on.
> 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.
>
> An example project that uses this setup can be found here:
> https://github.com/metaborg/mj.agda
> Check the makefile and the .agda-lib file
>
> Arjen
>
> On 02/16/2018 09:59 AM, Frederik Hanghøj Iversen 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 listAgda at lists.chalmers.sehttps://lists.chalmers.se/mailman/listinfo/agda
>
>
>


-- 
Regards
*Frederik Hanghøj Iversen*
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180216/ec9b41e7/attachment.html>