[Agda] Installing libraries

[Frederik Hanghøj Iversen]

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*
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20171110/8138ae2e/attachment.html>