<div dir="ltr">There is a recent packaging experiment in Coq:<br><div><br><a href="http://opam.ocaml.org/packages/coq/coq.8.4pl2/">http://opam.ocaml.org/packages/coq/coq.8.4pl2/</a><br></div></div><div class="gmail_extra">
<br><br><div class="gmail_quote">On Mon, Mar 24, 2014 at 11:02 PM, Mateusz Kowalczyk <span dir="ltr"><<a href="mailto:fuuzetsu@fuuzetsu.co.uk" target="_blank">fuuzetsu@fuuzetsu.co.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div class="">On 24/03/14 21:07, Andreas Abel wrote:<br>
> On <a href="tel:24.03.2014%2021" value="+12403201421">24.03.2014 21</a>:14, Mateusz Kowalczyk wrote:<br>
>> On 24/03/14 20:07, Andreas Abel wrote:<br>
>>> Mateusz, great initiative!<br>
>>><br>
>>> We would love to a have a version of cabal/hackage for Agda!<br>
>>><br>
>>> If you are motivated to work on this, it would make sense that<br>
>>> you join the Agda meeting in Paris in May (just announced!), or<br>
>>> come for a visit to Chalmers.<br>
><br>
>> While I'd love to attend, I doubt I'll be able to do so mostly due<br>
>> to financial constraints. I'm pretty sure my exams are at that time<br>
>> too.<br>
><br>
>> I would be interested in working on such tools but I doubt I could<br>
>> do it all alone so if anyone is interested and/or has ideas then<br>
>> I'm interested to hear about it! Personally I think that the best<br>
>> approach would be to take existing Hackage/cabal code and adapt it<br>
>> to Agda's needs but maybe there are some exciting new ideas that I<br>
>> don't know about.<br>
><br>
> Darin Morrison started on this a couple of years ago, but I think he<br>
> abandoned the project. You could ask him for advice.<br>
><br>
> <a href="https://github.com/darinmorrison" target="_blank">https://github.com/darinmorrison</a><br>
><br>
> Ulf Norell had some ideas about a minimal effort way of using cabal<br>
> for Agda, you could email him.<br>
><br>
><br>
<br>
</div>I'm CC'ing both although I'm not sure if Darin is on the list.<br>
<br>
I think if we are to re-use cabal then most of the work will be simply<br>
getting rid of irrelevant code.<br>
<br>
I'm also quite tempted by the idea of writing part of these tools in<br>
Agda but I don't know how practical that would be: we don't want to<br>
spend next 20 years writing something too slow to use but I think that<br>
maybe small parts would be nice. Are there any publicly available<br>
examples of such usage?<br>
<span class="HOEnZb"><font color="#888888"><br>
--<br>
Mateusz K.<br>
</font></span><div class="HOEnZb"><div class="h5">_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>