Custom setup for metatheory
This adds a custom setup to the metatheory package, which adds a hook to call Agda to
generate the Haskell source before building. Concretely, `cabal build
plc-agda` should now work (modulo caveats below).
This *requires* having the right Agda on the path already. I've provided
this in our `shell.nix`, so it will work from there, but it will
continue to not work outside it. There's not much we can do about this:
there's no good way to declare a dependency on Agda that cabal
understands, especially not since we also need the standard library.
Along the way, I rewrote our Agda building to use the Agda builders from
`nixpkgs-unstable`, which handle the recent changes to
`--local-interfaces` better, and also work properly with library files
(and we do have a checked in library file for our Agda, which we
previously had to throw away!).
As a bonus, we no long have to do the Nix cleverness that I had before
where we replaced the source of `plc-agda` with the generated Haskell.
Instead, we just provide the right Agda and let `cabal` generate the
Haskell source as part of a build hook.
(Aren't custom setups a pain? Yes: for cross-compilation, which we
don't care about for this package.)