<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">&lt;<a href="mailto:fuuzetsu@fuuzetsu.co.uk" target="_blank">fuuzetsu@fuuzetsu.co.uk</a>&gt;</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>
&gt; On <a href="tel:24.03.2014%2021" value="+12403201421">24.03.2014 21</a>:14, Mateusz Kowalczyk wrote:<br>
&gt;&gt; On 24/03/14 20:07, Andreas Abel wrote:<br>
&gt;&gt;&gt; Mateusz, great initiative!<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; We would love to a have a version of cabal/hackage for Agda!<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; If you are motivated to work on this, it would make sense that<br>
&gt;&gt;&gt; you join the Agda meeting in Paris in May (just announced!), or<br>
&gt;&gt;&gt; come for a visit to Chalmers.<br>
&gt;<br>
&gt;&gt; While I&#39;d love to attend, I doubt I&#39;ll be able to do so mostly due<br>
&gt;&gt; to financial constraints. I&#39;m pretty sure my exams are at that time<br>
&gt;&gt; too.<br>
&gt;<br>
&gt;&gt; I would be interested in working on such tools but I doubt I could<br>
&gt;&gt; do it all alone so if anyone is interested and/or has ideas then<br>
&gt;&gt; I&#39;m interested to hear about it! Personally I think that the best<br>
&gt;&gt; approach would be to take existing Hackage/cabal code and adapt it<br>
&gt;&gt; to Agda&#39;s needs but maybe there are some exciting new ideas that I<br>
&gt;&gt; don&#39;t know about.<br>
&gt;<br>
&gt; Darin Morrison started on this a couple of years ago, but I think he<br>
&gt; abandoned the project.  You could ask him for advice.<br>
&gt;<br>
&gt;   <a href="https://github.com/darinmorrison" target="_blank">https://github.com/darinmorrison</a><br>
&gt;<br>
&gt; Ulf Norell had some ideas about a minimal effort way of using cabal<br>
&gt; for Agda, you could email him.<br>
&gt;<br>
&gt;<br>
<br>
</div>I&#39;m CC&#39;ing both although I&#39;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&#39;m also quite tempted by the idea of writing part of these tools in<br>
Agda but I don&#39;t know how practical that would be: we don&#39;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>