travis-ci/{push,pr}

Stream: general

[Johan Commelin]

What is the difference between travis-ci/push and travis-ci/pr?
See e.g. https://github.com/leanprover-community/mathlib/pull/973
Why do we need both checks?

[Chris Hughes]

push checks the branch and pr checks whether it works after rebasing with current master. We don't need both, but apparently it's hard to switch off.

[Johan Commelin]

That's really silly that Travis doesn't have a switch for that :sad:

[Johan Commelin]

Shouldn't we turn this switch off: https://docs.travis-ci.com/user/web-ui/#build-pushed-branches

[Johan Commelin]

It means that Travis will not check commits that are pushed to branches that have not yet been PR'd.

[Johan Commelin]

That would be fine with me.

[Johan Commelin]

@Simon Hudon Do you know if that would work?

[Patrick Massot]

I'm all in favor of not Travis-checking branches that are not PR'ed. For instance, I'm creating a lot of noise in the Travis thread, and a lot of useless Travis work this afternoon

[Chris Hughes]

A lot of these issues could be solved if we just made a fork for WIP. I think PRing from branches is an unusual setup, so it makes it hard to work with travis and mergify.

[Johan Commelin]

I flipped this switch on the perfectoid project. Now we have https://github.com/leanprover-community/lean-perfectoid-spaces/pull/34

[Johan Commelin]

Only one check. Which is what we want.

[Johan Commelin]

Hmm, and now both checks are back... even though the switch is still disabled. (Github displayed two tests, for some weird reason. But after a hard refresh there was only one test.)