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

[Mateusz Kowalczyk]

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.