Procedure for PRs

Stream: general

[Neil Strickland]

I made my first attempt at a PR today 934 and got a build error that seems spurious. I see that @Simon Hudon has made another PR 936 which changes the build testing process, presumably to fix this problem. The root cause seems to be that I read the how to contribute page and the linked page on fork-and-branch workflow, and following those instructions, made my changes in a new fork of mathlib at https://github.com/NeilStrickland/mathlib. But I see that none of the other open PRs are doing that, they just come from branches of leanprover-community/mathlib. Are those instructions considered to be outdated? If so, is there anything newer? Would I need permissions to work with branches of leanprover-community/mathlib?

[Kevin Buzzard]

Both are supposed to work. The fork-and-branch workflow should say this, really.

[Kevin Buzzard]

And yes, I think you need permission (and I have no idea how I got it)

[Kevin Buzzard]

It got merged anyway :D Now about that predicate? :-) I mentioned it in my AITP talk

[Scott Morrison]

It's a known problem, which @Simon Hudon I think knows how to fix. The travis build tests the "development scripts", like update-mathlib and cache-olean. The test it runs often fails when run on a PR from a fork, because of the rate-limiter on the github API.

The intention is to disable these tests when travis runs a PR from a fork, but this hasn't happened yet. Sorry about the confusion this is causing.

[Simon Hudon]

I just merged that branch