<div dir="ltr"><div>I was considering that it might be possible to use cabal packages (and cabal) out-of-the-box. We'd just need some Distribution.Agda functions to use in Setup.hs to type check and install the Agda files. We are already doing something like this for Agda.Primitive in the Agda cabal package.<br>
<br></div>/ Ulf<br></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Mon, Mar 24, 2014 at 11:06 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="HOEnZb"><div class="h5">On 24/03/14 21:02, Tillmann Rendel wrote:<br>
> Hi,<br>
><br>
> Mateusz Kowalczyk wrote:<br>
>> Are there plans to assimilate tools with functionality of Hackage,<br>
>> Hoogle, Haddock and Cabal into the Agda environment?<br>
><br>
> This would be great!<br>
><br>
> Maybe a first step would be to define a notion of "Agda package" that<br>
> consists of a bunch of agda files. The goal would be to say:<br>
><br>
> agda --package stdlib Main.agda<br>
><br>
> instead of<br>
><br>
> agda -i$HOME/agda-lib/src -i. Main.agda<br>
><br>
> This is intentionally a very modest goal, but I think it would be a step<br>
> in a good direction.<br>
><br>
> Tillmann<br>
> _______________________________________________<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>
><br>
<br>
</div></div>I think we can re-use cabal packages for this pretty easily, removing<br>
anything we might not need. I think that what you outline is a fine<br>
first ‘big’ goal.<br>
<br>
I'll have to study the cabal source code.<br>
<br>
I am glad to see that there's interest.<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>