[Agda] Agda environment: Hackage, Hoogle, Haddock, Cabal?

Bas Spitters b.a.w.spitters at gmail.com
Mon Mar 24 23:32:42 CET 2014


There is a recent packaging experiment in Coq:

http://opam.ocaml.org/packages/coq/coq.8.4pl2/


On Mon, Mar 24, 2014 at 11:02 PM, Mateusz Kowalczyk <fuuzetsu at fuuzetsu.co.uk
> wrote:

> On 24/03/14 21:07, Andreas Abel wrote:
> > On 24.03.2014 21:14, Mateusz Kowalczyk wrote:
> >> On 24/03/14 20:07, Andreas Abel wrote:
> >>> Mateusz, great initiative!
> >>>
> >>> We would love to a have a version of cabal/hackage for Agda!
> >>>
> >>> If you are motivated to work on this, it would make sense that
> >>> you join the Agda meeting in Paris in May (just announced!), or
> >>> come for a visit to Chalmers.
> >
> >> While I'd love to attend, I doubt I'll be able to do so mostly due
> >> to financial constraints. I'm pretty sure my exams are at that time
> >> too.
> >
> >> I would be interested in working on such tools but I doubt I could
> >> do it all alone so if anyone is interested and/or has ideas then
> >> I'm interested to hear about it! Personally I think that the best
> >> approach would be to take existing Hackage/cabal code and adapt it
> >> to Agda's needs but maybe there are some exciting new ideas that I
> >> don't know about.
> >
> > Darin Morrison started on this a couple of years ago, but I think he
> > abandoned the project.  You could ask him for advice.
> >
> >   https://github.com/darinmorrison
> >
> > Ulf Norell had some ideas about a minimal effort way of using cabal
> > for Agda, you could email him.
> >
> >
>
> I'm CC'ing both although I'm not sure if Darin is on the list.
>
> I think if we are to re-use cabal then most of the work will be simply
> getting rid of irrelevant code.
>
> I'm also quite tempted by the idea of writing part of these tools in
> Agda but I don't know how practical that would be: we don't want to
> spend next 20 years writing something too slow to use but I think that
> maybe small parts would be nice. Are there any publicly available
> examples of such usage?
>
> --
> Mateusz K.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140324/fd25d820/attachment.html


More information about the Agda mailing list