AppVeyor build failing

Stream: general

[Scott Morrison]

Hi @Simon Hudon, could you have a look at https://github.com/leanprover-community/mathlib/pull/910 for me? The AppVeyor build has failed, and I don't know what to do about this. Having steps to the PR that mysteriously fail is no good. :-( It's hard enough already.

[Bryan Gin-ge Chen]

The issue seems to be that the update-mathlib test makes several requests to the github API and this is being rate-limited. (This seems to be hitting several other PRs as well).

[Scott Morrison]

I'd really like to see these script tests disabled for PRs that don't modify the scripts.

[Simon Hudon]

Yeah, the thing is that we can do that for travis but even if we don't run those tests, GitHub will expect a successful AppVeyor test

[Bryan Gin-ge Chen]

Can we wrap the appveyor script in some fancy git diff conditional?

[Bryan Gin-ge Chen]

Maybe something like if [[ -n $(git diff HEAD master scripts/)]]

[Bryan Gin-ge Chen]

Oh wait, I guess there's some commented out lines that do the same thing.

[Simon Hudon]

that's try but you need to make a trivial build happen when those conditions aren't satisfied.

[Scott Morrison]

What is the work-around at the moment? Several of my PRs are red because of AppVeyor, and I don't know what to do.

[Simon Hudon]

Which ones?

[Scott Morrison]

https://github.com/leanprover-community/mathlib/pull/926

[Scott Morrison]

https://github.com/leanprover-community/mathlib/pull/935

[Scott Morrison]

https://github.com/leanprover-community/mathlib/pull/931

[Scott Morrison]

https://github.com/leanprover-community/mathlib/pull/926

[Simon Hudon]

I made a change on AppVeyor which I thought was already there. PRs from leanprover-community should no longer have this issue.

[Simon Hudon]

All good?

[Patrick Massot]

All good?

No: https://ci.appveyor.com/project/cipher1024/mathlib/branch/master

[Patrick Massot]

This is not a PR, this is mathlib master

[Scott Morrison]

I just had another AppVeyor failure testing update-mathlib on a "just maths" PR.

[Scott Morrison]

https://ci.appveyor.com/project/cipher1024/mathlib-3r2np/builds/24320557/job/wuq0ved0jo40eybs

[Simon Hudon]

Solved

[Scott Morrison]

And today an update-mathlib failure on travis: https://travis-ci.org/leanprover-community/mathlib/jobs/528680165

[Johan Commelin]

If I click that link, I don't see the failure :sad: Did someone restart the build?

[Scott Morrison]

Ah, I restarted it. I thought the URL would point to the old build, still.

[Johan Commelin]

I looked a bit, but couldn't easily find the logs for the old build. (I'm on a flaky connection, so clicking links isn't very fast...)

[Mario Carneiro]

It's tricky to get build logs from restarted builds. I think the data exists but you have to talk to Travis people

[Mario Carneiro]

https://github.com/travis-ci/travis-ci/issues/2993

[Johan Commelin]

@Simon Hudon Here is another misbehaving critter: #993

[Sebastien Gouezel]

Also #966

[Johan Commelin]

The AppVeyor test is only there to test things on a certain OS developed in Redmond, right?

[Simon Hudon]

That's right. That's the one reason

[Simon Hudon]

@Sebastien Gouezel and @Johan Commelin how long ago did you merge with master?

[Sebastien Gouezel]

Github says: 20 hours ago.

[Johan Commelin]

Same for me... should be somewhere in the last 30 hours.

[Simon Hudon]

That's odd

[Simon Hudon]

Ok, I'll look into it

[Johan Commelin]

Thanks!

[Simon Hudon]

@Sebastien Gouezel In the travis file, where you see

      if: type != pull_request OR head_repo = leanprover-community/mathlib
      if: type != cron

can you replace it with this?

      if: type != cron && (type != pull_request OR head_repo = leanprover-community/mathlib)

[Sebastien Gouezel]

Done. Let's see if it makes a difference.

[Simon Hudon]

You only replaced it once. It's there four times

[Sebastien Gouezel]

Oh, crap. Done again, hopefully I didn't miss one this time.

[Simon Hudon]

You can see that you didn't miss one by looking: https://travis-ci.org/leanprover-community/mathlib/builds/530898018. All the script testing has been disabled.