[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

[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 <

Post by 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
name: my-project
funky-dep
src
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
https://lists.chalmers.se/mailman/listinfo/agda

[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

Post by 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
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
name: my-project
  funky-dep
  src
  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]).
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
https://lists.chalmers.se/mailman/listinfo/agda
<https://lists.chalmers.se/mailman/listinfo/agda>
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Nils Anders Danielsson]

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.

One can already give the path to the library file on the command line.
However, I think the paths in that file have to be absolute. Perhaps
they could also be allowed to be relative to the location of the file.