[Agda] Finer-grained library control in Agda

[Frederik Hanghøj Iversen]

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.

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

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.
https://github.com/metaborg/mj.agda
Check the makefile and the .agda-lib file
Arjen
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*
_______________________________________________

[Ulf Norell]

I'm not sure I understand your problem exactly, but note that registering a
package in `~/.agda/libraries` only makes it available as a possible
dependency. As long as the library name doesn't clash with other libraries
and you don't add it to `~/.agda/defaults` it will not interfere with other
libraries. In your case it should be enough to rename the modified version
of the standard library (or add a special version number [1]).

/ Ulf

[1]
http://agda.readthedocs.io/en/latest/tools/package-system.html#version-numbers

On Fri, Feb 16, 2018 at 9:59 AM, Frederik HanghÞj Iversen <

Post by Frederik Hanghøj Iversen
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 list
https://lists.chalmers.se/mailman/listinfo/agda