[Agda-dev] Agda and Packages/Libraries

[Philipp Hausmann]

On 02/04/2016 03:38 PM, Nils Anders Danielsson wrote:
> On 2016-02-04 14:44, Philipp Hausmann wrote:
>> It would also be possible to publish the generated Cabal packages on
>> Hackage, but they would just be plain Haskell packages. If you want to
>> expose an Agda library as a normal Haskell/Cabal package using FFI
>> exports, this is good enough.
>
> What if, say, support for a newer version of GHC is added to MAlonzo? A
> person who knows nothing about Agda might have a hard time recompiling
> the Agda sources (which might not even be available).
>
Good question :-) There is also the question what to do about
Haskell-dependencies.
E.g. if I write a Agda wrapper for the containers Haskell package, we
need to make sure
containers is installed. Do we use cabal or stack for that? If stack, what
LTS/snapshot version?
So indeed, compilation with GHC is a bit tricky. That's why I decided to
make this somebody else's
problem(tm). My proposal assumes that all necessary Haskell packages are
already installed
and that a suitable GHC is available. A tool like Agda-Stack, which
could be built on top of this,
would then create an Agda package DB for each Agda/GHC version
combination in use:

~/Agda-2.5/ghc-7.10/
~/Agda-2.5/ghc-7.8/

In principle, one could also share the generated *.agdai interfaces for
all target GHC's. We don't
have anything like CPP, so this should work, not sure if it would be a
good idea though.

And as if it weren't complicated enough, there is also the JS backend...
However, I think
the JS backend shouldn't really be a problem as it doesn't need compilation.

My long term goal is that a user can just simply use the Agda
environment like Haskell/Stack
where all the dependencies are automatically downloaded. My proposal is
merely a step in that
direction and adds some of the building blocks for that, but is
definitely not the final answer.
But solving all packaging problems requires a lot of time, so it's
probably better to start simple
and do one thing at a time.

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/20160204/7b47199a/signature.bin