[Agda-dev] Agda and Packages/Libraries

[Philipp Hausmann]

Hi,

In the last month or two, I have been playing around with the idea of
adding a Package system to
Agda proper. I think Ulf's library system is definitely a step in the
right direction, but there is still
room for improvement. Especially when compiling Agda programs using
MAlonzo, things
get tricky fast.

I now basically have a prototype implementation of a very basic
packaging system which
features a simple build tool similar to Haskell's Setup.hs. This is all
still quite low-level, this is *not*
stack or cabal, only Setup.hs. So it can build & install a single
package, but it
doesn't do dependency solving nor does it download any missing Agda or
Haskell packages.

While it uses cabal under the hood, in my proposed solution Agda
packages are
*not* Haskell packages; however, you can generate Haskell packages from Agda
packages. Having a completely unified Agda/Haskell Package system might
be a nice goal,
but it would make the implementation much more complicated and I don't
think it's worth the effort (right now).


A small example how this could be used (the build tool is called "fauchi") :


# create a new Agda package db
fauchi init-pkg-db PATH

# install the Agda Haskell support libraries for MAlonzo
fauchi install-agda-ghc-rte --agda-package-db PATH

# install the Agda primitives module (includes ghc compilation)
fauchi install-primitives --agda-package-db PATH

# Assuming we are in the std-lib dir, and that
# a agda-pkg.yaml package description file exists,
# we can then build the standard library:
fauchi build --agda-package-db PATH


It would still be possible to use Agda the conventional way with include
paths, so it would be
completely opt-in. Nonetheless, one could implement some more convenient
tools on top of this.
E.g. I think this would go along nicely with the Nix package manager,
but it is also possible
to implement something like "stack" on top of this.

This is all still unfinished and work-in-progress. But before I invest
more time in this, I wanted to hear what you think about this?
What are the chances of merging something like this?

(If you really want to look at the code, it is here:
https://github.com/phile314/agda/commit/f7bfb92c941ae845e9ff58f3a1aa652cb447fb58
But you've been warned, this is still a prototype!
)

Cheers,
Philipp

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
Url : http://lists.chalmers.se/pipermail/agda-dev/attachments/20160203/c58f5b29/signature.bin