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

[Stevan Andjelkovic]

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.