[Agda] Installing libraries

[a.j.rouvoet]

At some point I was looking for similar functionality, but am very 
content now using git sub-modules for tracking
specific versions of "funky" dependencies in the project repository.

Assuming you are using git and that your dependencies are tracked in 
git, this makes it very easy to pull in the
correct versions and instead of using the 'depend' key in your .agda-lib 
file, you use the project-root relative
include paths.

For an example see the following .agda-lib file and makefile in this 
repository [1].
The makefile is set up to do all the work for you when you run `make`.

[1]: https://github.com/metaborg/mj.agda/

Cheers,


Arjen

On 11/10/2017 07:24 PM, Ulf Norell wrote:
> 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 <mailto: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
>     <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 <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>     <https://lists.chalmers.se/mailman/listinfo/agda>
>
>
>
>
> _______________________________________________
> 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/20171111/81b20f27/attachment.html>