How to keep travis happy?

[andres-erbsen]

We want to keep the travis-CI builds passing, both for our own convenience of working on master and because coq uses fiat-crypto#master as an integration test. This issue is about how to avoid needless failing travis builds. #116 was my fault, but this is not the first time we have optimistically merged something to master in hope that it will work, and saw that it actually didn't build. Ideally, we would fully re-build and test before we push. However, "just test it first" is probably not the best idea given that a complete build on one version takes roughly half an hour. Here are some other ideas on improving this general situation.

• First, let's just not put code that we already know would make travis unhappy on master. If it is a good idea to merge code that would break things, it is probably also a good idea to re-write or disable the broken things.
• Maybe we should have a Makefile target that removes files that would not be present in a clean build. This would prevent the (not that uncommon) failure mode of the build passing on our own machines due to pre-existing .vo files which are not actually built on travis. I don't know how easy it would be to implement this.
• If we really wanted to make sure master makes travis happy all the time, we could have github disallow pushes to master altogether, and require github-orchestrated merges to pass travis checks before they can be merged. This, of course, would be somewhat annoying, but it wouldn't cause huge issues with my personal workflow. @JasonGross , @jadephilipoom ?

[JasonGross]

#116 could have been avoided by noticing that #115 had a little red x next to the commit marker. I say, at the least, we make it a policy to not merge PRs unless Travis is happy with them as PRs.

Maybe we should have a Makefile target that removes files that would not be present in a clean build. This would prevent the (not that uncommon) failure mode of the build passing on our own machines due to pre-existing .vo files which are not actually built on travis. I don't know how easy it would be to implement this.

The target is called update-_CoqProject :-P This will not fix an issue of .v files that you forgot to git add, only missing .vo files. So I suppose we could have a target that does some bash wizardry to get things in find . -name "*.v" and not in $(VFILES) and then append o and separately append .d and then remove them.

If we want something stronger, there's some arcane wizardry that Anders wrote in etc/coq-scripts/Makefile.coq.common, I believe, by the name of vo_closure and the FORCE target, which can have the build fail if there are transitive .v dependencies not tracked by git. Last time I set this up, I seem to recall you saying that you didn't want our Makefile to depend on git submodule directories, and I'd argue that this is complicated enough that we don't want to copy-paste it.

we could have github disallow pushes to master altogether, and require github-orchestrated merges to pass travis checks before they can be merged.

This would interfere with my workflow, though I could be convinced.

[andres-erbsen]

I agree that #116 was completely avoidable; I agree that just making going through the (not that significant) effort of checking travis status indicators before merging branches that have already been built by travis would improve things.

The Makefile wizardry you mentioned indeed looks quite arcane, I think we can do without it (except, maybe if it was a part of coq_makefile, but that is not the case).

I guess "don't fuck up" isn't that satisfying a resolution, but if we can't come up with anything that would fit our overall preferences than that, I guess that's what we will do. I will leave this issue open for a bit, just in case we have anything to add.

[andres-erbsen]

Also, about PR-s: I believe travis being happy with a PR does not actually mean that the merged version will build. Am I correct on this?

[JasonGross]

Am I correct on this?

Yes, because merge is not a no-op. Travis tests the branch, not the merged version. We can potentially fix this by having Travis merge origin/master into the current branch before building; we'd want this as a separate build line item, because otherwise you'll get confused about why you can't locally reproduce the Travis build failure.

[JasonGross]

Also, if you enable Travis on your fork of the repo, I believe you will (or can configure it to) get emails when your branches fail to build.

[jadephilipoom]

If we really wanted to make sure master makes travis happy all the time, we could have github disallow pushes to master altogether, and require github-orchestrated merges to pass travis checks before they can be merged.

This option seems by far the most reasonable to me, and would not interrupt my workflow.

[andres-erbsen]

Closing due to inactivity.