[Agda] Re: The standard library has moved to github

Jason Gross jasongross9 at gmail.com
Sun Jan 19 22:27:14 CET 2014


$ time darcs get --lazy http://code.haskell.org/Agda
Finished getting.

real    0m25.181s
user    0m1.952s
sys     0m2.200s

This is on a computer that is around 4 times faster than the travis
machines, and is on MIT's internet.  I could believe that the travis
machines on slower internet will take around 10 minutes to get the
Agda repo.

On Sun, Jan 19, 2014 at 1:32 PM, Stevan Andjelkovic
<stevan.andjelkovic at strath.ac.uk> wrote:
> On Sun, Jan 19, 2014 at 01:05:23PM -0500, Jason Gross wrote:
>> You can hack around this by making a script that does "while 1; do
>> sleep 2m; done" and spawn it in the background and kill it when you're
>> done.  The HoTT/HoTT library does this, because we have some files
>> that take around 15 minutes to typecheck.  You still have a hard cap
>> of 60 minutes, though.
>
> Darcs getting the Agda repo shouldn't take more than a couple of
> seconds, so when it takes over 10 mins (as it did when I tried)
> something must be wrong, I figure.
>
> I can see this trick being useful in situations further down the road
> though, thanks.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


More information about the Agda mailing list