github actions

Stream: general

[Sebastien Gouezel]

We have recently switched to github actions instead of Travis. Now, even on my fork, all branches get built. If I understand correctly, this is because the file build.yml got copied when I updated master.

I often push work in progress to github, to save it. Now, github tries to build this work in progress, which a crazy waste of processor time. Moreover, it tries to build it both on 3.4.2 and nightlies, which is a double waste. I tried to use commit messages with [ci skip], but to no avail.

Do you see a way I could improve my workflow?

[Gabriel Ebner]

If you don't want your branches to be built, you can disable github actions (for your repository) at https://github.com/sgouezel/mathlib/settings/actions

[Gabriel Ebner]

I can't comment on the "waste of resources" part. The mathlib build only takes a fraction of the time limit set by github, they clearly seem to expect this usage. Are there any downsides to building mathlib with multiple lean versions? Do you get inundated with emails?

[Kevin Buzzard]

Are there any downsides to building mathlib with multiple lean versions?

Doesn't it harm the environment or something?

[Johan Commelin]

It probably does. I don't think GitHub Actions is CO₂-neutral

[Sebastien Gouezel]

Yes, that's my point. Thanks @Gabriel Ebner , I have desactivated actions on my fork.

[Sebastien Gouezel]

Also, mathlib master is currently broken (error in \archive\cubing_a_cube.lean). I guess the new building tools do not test archive properly...

[Johan Commelin]

Ouch... that happened quickly (-;

[Johan Commelin]

Anyway, better discover it now instead of 3 months from now

[Sebastien Gouezel]

If you go to https://github.com/leanprover-community/mathlib/runs/409812707 for instance, the test step seems to succeed, but if you open it you will see an error.

[Johan Commelin]

Also:

leanpkg build                          1h 16m 7s
> lean --make src
Run leanpkg build | python scripts/detect_errors.py

WARNING: Lean version mismatch: installed version is nightly-2020-01-12, but package requires 3.4.2

configuring mathlib 0.1

WARNING: Lean version mismatch: installed version is nightly-2020-01-12, but package requires 3.4.2

> lean --make src

[Gabriel Ebner]

Re: broken archive file. See https://github.com/leanprover-community/mathlib/pull/1911

[Rob Lewis]

@Johan Commelin Are you worried about the warnings? Right now 3.5c should be backward compatible and we want to test with both. Once we officially bump mathlib we'll drop the 3.4.2 test (and package requirement).

[Rob Lewis]

#1912 to fix the archive.

[Johan Commelin]

Ok, if the warnings are deliberately ignored, I'm fine with that. :grinning_face_with_smiling_eyes:

[Bryan Gin-ge Chen]

More pressing is the fact that there is some authentication issue causing pushes to mathlib-nightly to fail, so that update-mathlib is fetching a commit that's a few days out of date. I also had a question here about why each PR commit triggers 4 github actions runs.

[Rob Lewis]

We're working on the authentication thing.

[Rob Lewis]

I briefly looked around and didn't see an easy fix for the duplicated builds on a PR from a branch.

[Rob Lewis]

We could disable branch builds. But once we're storing build artifacts, we might want them.

[Gabriel Ebner]

We're failing later than ever before: :tada: https://github.com/leanprover-community/mathlib/runs/413414692

[Gabriel Ebner]

Now we get:

++ git push mathlib HEAD:refs/heads/lean-3.4.2
remote: Permission to leanprover-community/mathlib.git denied to leanprover-community-bot.

[Gabriel Ebner]

As well as:

++ git push nightly HEAD:mathlib-master
To https://github.com/leanprover-community/mathlib-nightly.git
 ! [rejected]          HEAD -> mathlib-master (non-fast-forward)
error: failed to push some refs to '***github.com/leanprover-community/mathlib-nightly.git'
hint: Updates were rejected because a pushed branch tip is behind its remote
hint: counterpart. Check out this branch and integrate the remote changes
hint: (e.g. 'git pull ...') before pushing again.
hint: See the 'Note about fast-forwards' in 'git push --help' for details.

[Gabriel Ebner]

And:

++ git push nightly tag nightly-2020-01-28
To https://github.com/leanprover-community/mathlib-nightly.git
 ! [remote rejected]   nightly-2020-01-28 -> nightly-2020-01-28 (shallow update not allowed)

[Rob Lewis]

The 3.4.2 failure is because of a branch protection rule, I just added leanprover-community-bot to the access list.

[Rob Lewis]

Absolutely no idea about the others. I guess we need to add a git log to see what it's trying to push?

[Gabriel Ebner]

https://github.com/leanprover-community/mathlib/pull/1919 <-- this should fix the rest

[Rob Lewis]

That fixes the "branch tip is behind its remote" error?

[Rob Lewis]

Okay, yeah, I guess it sounds plausible.

[Gabriel Ebner]

I'm not sure either.

[Rob Lewis]

Well, fingers crossed once again.

[Gabriel Ebner]

Damn, almost there. Can anybody please delete the nightly-2020-01-28 tag in the nightlies repo (ideally within 60 minutes)? The script managed to create the tag but didn't upload the tarballs. @Rob Lewis @Simon Hudon

[Rob Lewis]

Done.

[Gabriel Ebner]

Thank you!

[Rob Lewis]

It looks like there's still some kind of branch protection problem though?

[Gabriel Ebner]

I've already fixed it.

[Rob Lewis]

Ah, cool.

[Gabriel Ebner]

Oops, forgot to click "save changes". Thanks for making me look at the settings page again.

[Rob Lewis]

:tada:

[Rob Lewis]

Thanks Gabriel!

[Rob Lewis]

What's the purpose of the install olean-rs state of the build script? I don't see where it's being used.

[Rob Lewis]

I guess it's related to #687. It was present in the Travis script but doesn't seem to be used there either.

[Simon Hudon]

There was a time where it was used to check mathlib but the error messages irritated people more than it helped them so it got disabled.

[Mario Carneiro]

Maybe turn it on again to see if it is broken?

[Rob Lewis]

I'll run it locally to see what it says. Probably better to remove it completely from CI for now.

[Rob Lewis]

Should we remove the 3.5c nightly build from CI? I think this is asking for trouble if/when breaking changes make it into 3.5c. We should be following a release schedule there and updating mathlib to be compatible with each release.

[Bryan Gin-ge Chen]

There's now an API for downloading GitHub Actions Artifacts. I think it should be possible now to use this to make cache-olean --fetch work with PR branches. Does anyone (else) want to take a shot at it?

[Rob Lewis]

Oh, wow, that happened a lot sooner than I expected.

[Rob Lewis]

I was planning to look into external hosting for olean caches in the next few weeks. But if this works it could be easier.

[Rob Lewis]

Not sure how much trouble the API rate limiting will cause.

[Patrick Massot]

Can't we use GitHub authentication to have a higher rate?

[Rob Lewis]

If you want to try it out, feel free, I don't think I'll have time this week.

[Rob Lewis]

Patrick Massot said:

Can't we use GitHub authentication to have a higher rate?

Maybe, no idea.

[Gabriel Ebner]

Yeah, please go for it.

[Patrick Massot]

I'll try to find time for the bundle thing, so I'll leave cache-olean to Bryan. Note that any work on this should probably start with fixing the huge UX bug in cache-olean and update-mathlib that we talk to GitHub before trying to find a local archive.

[Bryan Gin-ge Chen]

It looks like Github authentication is required to use any of the Github actions API endpoints, so cache-olean users who want to download artifacts will have to supply a personal access token somehow.

[Patrick Massot]

What about trying to do what elan does to avoid using this API?

[Patrick Massot]

In the case of mathlib nightlies we can even directly use the url which is predictable

[Bryan Gin-ge Chen]

As far as I can tell the github artifact URLs for each PR are not really predictable.

[Bryan Gin-ge Chen]

The alternative would be to upload all generated olean files to some server that we control. I believe this was the original plan when it was still unclear whether / when an official github artifact API would become available.

[Rob Lewis]

I guess cache-olean and update-mathlib could ask the user to give a token during installation? It could be optional, and if there's no token they could default to the current behavior.

[Rob Lewis]

It would probably be asking for trouble to generate a default PAT ourselves, right?

[Patrick Massot]

What is a PAT?

[Rob Lewis]

An acronym I made up because I didn't want to type personal access token.

[Patrick Massot]

This all sounds a bit silly. It may be faster to work on other hosting solutions.

[Jasmin Blanchette]

Looks like a reference to Curry-Howard (Proof As Terms, Propositions As Types).