Making the Travis build faster and more robust

[Blaisorblade]

From https://travis-ci.org/agda/agda-stdlib/builds/102799931

$ openssl aes-256-cbc -K $encrypted_3f6e0f4132ed_key -iv $encrypted_3f6e0f4132ed_iv -in .dropbox_uploader.enc -out .dropbox_uploader -d
iv undefined
The command "openssl aes-256-cbc -K $encrypted_3f6e0f4132ed_key -iv $encrypted_3f6e0f4132ed_iv -in .dropbox_uploader.enc -out .dropbox_uploader -d" failed and exited with 1 during .

Not sure it matters, Travis was already broken as of #78.

[gallais]

I'll summarize the Travis situation as Matthew is going through old issues at the moment:

• We want to compile the html doc and host it on http://agda.github.io/agda-stdlib/
• In general stdlib's master needs Agda's master to compile (because e.g. new pragmas are introduced and an older version would choke on them)
• Building the latest Agda at every push is slow

The ideal solution would be to get Agda's Travis to upload an artefact after each successful build and make it available to all. This way stdlib (but also any other Agda library maintainer out there) can just pull the latest executable and use it to run its tests.

Now that Travis has build stages, it looks like it ought to be possible to have this deployment only happen when master is as bug-free as the test-suite can guarantee.

[MatthewDaggitt]

Thanks for the summary! Nice to know it's still being looked it. As I don't have much knowledge of either Travis or the Agda tests I might leave this to someone else more involved in the main Agda repository.

[gallais]

I've created the branch travis to try to see if we can get something basic running (it's simply pulling the latest master from agda/agda & compiling it so it's slow and prone to failure if master doesn't compile).

Given that we've been getting a lot of updates recently that'd at least give us newer documentation even if it'd take long.

[gallais]

Ok, so the build succeeded but apparently the upload was not successful. I'm not sure why. Could it be that the GH_TOKEN is invalid these days?

Edit: rather than using an encrypted variable, it seems we could just setup a variable in repository settings

[andreasabel]

Mmh, wouldn't the fetch already have failed if the token was invalid?

Maybe it is worth to remove the pipe into /dev/null in the last command

git push -q upstream HEAD:gh-pages &>/dev/null

to see whether this succeeded!?

[gallais]

Yup it's a credentials issue (happy to see that travis now censors this kind of information rather than leaking it via error messages):

remote: Invalid username or password.
fatal: Authentication failed for 'https://[secure]@github.com/agda/agda-stdlib.git/'

I guess the easiest solution is to setup a new github token (maybe directly in the repository settings?).

[andreasabel]

Yes, you are welcome to create a new token (maybe it has expired). And yes, I think it goes into the repo settings.

[gallais]

Oh wow, I didn't know I could modify these settings myself! It worked. I'll push a dummy commit to see whether the build is sped up by caching $HOME/.ghc and then I'll cleanup, squash and merge.

[gallais]

Pushed: 782f961

Hopefully this doesn't crash given all the tests I have run... It's still not completely satisfactory but it'll have to do until we get into the business of build stages.

[gallais]

Nowadays:

• master relies on the released version of Agda so caching works well
• experimental is slow but it points to a specific commit so we don't risk pulling a broken version of Agda

So I consider this to be solved. Making the build even faster is of course still
desirable but it's a different issue.