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

[Mateusz Kowalczyk]

On 19/01/14 13:16, Stevan Andjelkovic wrote:
> On Fri, Jan 17, 2014 at 11:41:16PM -0500, Jason Gross wrote:
>>    The [1]HoTT library uses [2]Travis to do continuous integration, and
>>    [3]build documentation and push it to gh-pages.  The travis setup we
>>    use is [4]here, and [5]this commit message describes how we generated
>>    the token that Travis needs.  If you run into trouble or need help, I
>>    can probably provide answers.
>>    (You could probably then just have that link redirect to the gh-pages
>>    generated version.)
> 
> Thanks Jason, that was really helpful.
> 
> This Travis thing is quite neat; basically it's like a virtual computer
> which you can install stuff on and then post-process your commits with
> -- build binaries, run tests, etc.
> 
> I tried to make a minimal example that would contain all the bits that
> generating the html listings for the std-lib would, you can find it
> here:
> 
>   https://github.com/stevana/test-generate-agda-html-via-travis
> 
> The idea is that every time a commit happens the html gets updated
> automatically by Travis. The file which makes this happen is:
> 
>   https://github.com/stevana/test-generate-agda-html-via-travis/blob/master/.travis.yml
> 
> I took the, pretty complex, HoTT example Jason linked to and simplify
> it as much as I could. I'm sure I made things less robust in the
> process, in particular I don't feel very confident about the git bits,
> but it seems to work.
> 
> Travis doesn't seem to like darcs, so I couldn't make it fetch and
> build the Agda development version. I suppose that won't be a problem
> once the Agda repo gets moved to github though.
> 
> So, unless someone knows how to get darcs working, I guess it's best to
> wait for the Agda repo move, once that's done it should hopefully not be
> much work to modify the above example to generate html listings for the
> standard library.
> 
> 
> Cheers,
> SA.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

You can install anything you want on these boxes. If you were unable to
get it going through Apt, you should try using cabal install instead.

-- 
Mateusz K.