[Agda] Installing libraries

[Ulf Norell]

One possibility might be to add support for local 'libraries' files. That
way you could distribute
your project together with a special libraries file for the funky
dependencies, without cluttering
the agda-lib file with explicit paths.

/ Ulf

On Fri, Nov 10, 2017 at 4:51 PM, Frederik Hanghøj Iversen <
fhi.1990 at gmail.com> wrote:

> 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?
>
> What I'm hoping for is the possibility to put something like the following
> in my .agda-lib file:
>
> name: my-project
> depend:
>   funky-dep
> include:
>   src
> libs:
>   path-to-funky-dep
>
> 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".
>
> 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.
>
> 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]).
>
> [1]: http://agda.readthedocs.io/en/v2.5.2/tools/package-
> system.html?highlight=agda-lib#installing-libraries
>
> --
> 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/20171110/519f7ed6/attachment.html>