[Agda] Agdckage

[Nils Anders Danielsson]

Hi,

Agda is now available on Hackage, so Agda and most of its dependencies
can be installed simply by running

  cabal install Agda

and, for the command-line program,

  cabal install Agda-executable.

(This assumes that some dependencies are installed: cabal-install, GHC
and some C library development files). However, libraries of code
written in Agda cannot be installed quite as easily.

Recently I spoke to Lennart Augustsson, who suggested that we could
use Cabal also for Agda code. I have looked into this, and it seems as
if, with relatively little effort, we could get a package system for
Agda. Outline of the idea:

* Agda sources can be listed as data-files in Cabal packages. They are
  installed in predictable locations which we can teach Agda about, so
  that --include-path does not need to be used quite as often. (In the
  simplest case, if we put minimal effort into this, installing several
  versions of the same library at the same time could lead to trouble
  for Agda.)

* We can depend on a specific version of Agda by listing it as a
  dependency. We can also depend on specific versions of Agda
  packages, as well as Haskell packages used by the FFI.

* A Cabal package also needs to contain Haskell code. This can be a
  program which, when run, type-checks the Agda code. We can provide
  boilerplate code in the Agda library to make this easy. One could also
  imagine giving this program the capability to uninstall the library,
  or at least to provide information about it. Perhaps it is also
  possible to use Template Haskell to type check the Agda code as part
  of the compilation process for the Haskell program.

* I do not think that we should put Agda code on Hackage, but it is
  possible to tell cabal-install to look for other repositories (one
  just has to add a line to ~/.cabal/config), so we can set up our own
  "Agdckage". Then it would be possible to install Agda library X, and
  all its dependencies, including Agda itself, by typing
    cabal install X.

What do you think? It feels like a bit of a hack, but implementing a
package system is not fun, so it would be good if we could take
advantage of the work others have put into this.

Needless to say, if someone can use some spare time to implement the
ideas above it would be a welcome contribution to the Agda project.

-- 
/NAD

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.