Using Travis CI to build stdlib's documentation

[gallais]

I've spent the last few days playing with travis to build various projects of mine and applied the newly acquired knowledge to Agda's standard library.

Here is the result
Here are the builds
Here is my repo with the appropriate scripts, travis file and cleaned up gh-pages branch.

Now, travis needs a token from a user allowed to push to the repository in order to deploy the pages so I can't really prepare a pull request that would work. I can either explain to someone how to replicate the work based on the state my repo is in or do it myself if you give me push rights.

Happy holidays,

[np]

I support you in getting push permission.

On 12/30/2014 07:53 PM, gallais wrote:

I've spent the last few days playing with travis to build various
projects of mine and applied the newly acquired knowledge to Agda's
standard library.

Here is the result http://gallais.github.io/agda-stdlib/
Here are the builds https://travis-ci.org/gallais/agda-stdlib/builds
Here is my repo https://github.com/gallais/agda-stdlib with the
appropriate scripts, travis file and cleaned up gh-pages branch.

Now, travis needs a token from a user allowed to push to the repository
in order to deploy the pages so I can't really prepare a pull request
that would work. I can either explain to someone how to replicate the
work based on the state my repo is in or do it myself if you give me
push rights.

Happy holidays,

—
Reply to this email directly or view it on GitHub
#45.

Best regards,
-- NP

[andreasabel]

Gallais,

thanks for the travis instance for the standard library!

I invited you to the Agda community.

Frankly, there is a small moment of hesitation as you do not use your
real name. I'd be more easy if I had a face to connect to a collaborator...

Cheers,
Andreas

On 30.12.2014 21:40, Nicolas Pouillard wrote:

I support you in getting push permission.

On 12/30/2014 07:53 PM, gallais wrote:

I've spent the last few days playing with travis to build various
projects of mine and applied the newly acquired knowledge to Agda's
standard library.

Here is the result http://gallais.github.io/agda-stdlib/
Here are the builds https://travis-ci.org/gallais/agda-stdlib/builds
Here is my repo https://github.com/gallais/agda-stdlib with the
appropriate scripts, travis file and cleaned up gh-pages branch.

Now, travis needs a token from a user allowed to push to the repository
in order to deploy the pages so I can't really prepare a pull request
that would work. I can either explain to someone how to replicate the
work based on the state my repo is in or do it myself if you give me
push rights.

Happy holidays,

—
Reply to this email directly or view it on GitHub
#45.

Best regards,
-- NP

—
Reply to this email directly or view it on GitHub
#45 (comment).

Andreas Abel <>< Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel@gu.se
http://www2.tcs.ifi.lmu.de/~abel/

[gallais]

I've slightly edited my profile to make it clearer that "gallais" really is just a convenient way of writing "G. Allais" as in "Guillaume Allais". Hope it clears any doubt. Thanks for the credentials!

[asr]

Which is the difference between the documentation generated via Travis and the documentation generated in the gh-pages branch (see https://github.com/agda/agda-stdlib/blob/gh-pages/README.md) ?

[gallais]

It's done automatically after each commit rather than manually by Ulf.

[asr]

Are you sure? Is Ulf manually generating the documentation after each commit?

[gallais]

Via a script AFAICT https://github.com/agda/agda-stdlib/blob/master/publish-listings.sh

[asr]

I see. Isn't it possible to write a post-commit hook in the server side to perform this task? (I don't see any problems to write the hook in the client side, but it is not a good solution).

[gallais]

If I'm not mistaken, this is precisely what travis is doing: every time a (group of) commit(s) is pushed, it spawns a VM which follows the script described by the .travis.yml file.

[UlfNorell]

I don't run the script manually obviously. I have a cron job that runs it every night. I'd be happy to turn that off and let Travis to the heavy lifting though.

[asr]

@gallais You are right.

[gallais]

Ok, I have pushed the version using a static executable built from agda/agda here: 532c76f

Someone with admin rights on the repository needs to turn travis builds on for agda/agda-stdlib here: https://travis-ci.org/profile/agda

Why a static executable? First of all because it guarantees that the build won't fail because agda/agda's master is in a state where agda cannot be built. Second of all, it cuts down the runtime by ~75% as witnessed by these two branches: https://travis-ci.org/gallais/agda-stdlib/branches

[andreasabel]

I just flipped the switch. Thanks, G.!