<div dir="ltr">Can I depend on a package only locally?<div><br></div><div>I know I can put a package in `~/.agda/libraries` and thus make it available globally on my system.</div><div><br></div><div>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.</div><div><br></div><div>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.</div><div><div><br></div>-- <br><div class="gmail_signature" data-smartmail="gmail_signature"><div>Regards</div><div><i>Frederik Hanghøj Iversen</i></div></div>
</div></div>