Zulip Chat Archive

Stream: general

Topic: github actions


Sebastien Gouezel (Jan 27 2020 at 11:02):

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 (Jan 27 2020 at 11:53):

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 (Jan 27 2020 at 11:56):

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 (Jan 27 2020 at 12:30):

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

Doesn't it harm the environment or something?

Johan Commelin (Jan 27 2020 at 12:30):

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

Sebastien Gouezel (Jan 27 2020 at 12:39):

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

Sebastien Gouezel (Jan 27 2020 at 12:43):

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 (Jan 27 2020 at 12:44):

Ouch... that happened quickly (-;

Johan Commelin (Jan 27 2020 at 12:44):

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

Sebastien Gouezel (Jan 27 2020 at 12:47):

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 (Jan 27 2020 at 12:49):

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 (Jan 27 2020 at 13:09):

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

Rob Lewis (Jan 27 2020 at 13:09):

@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 (Jan 27 2020 at 13:28):

#1912 to fix the archive.

Johan Commelin (Jan 27 2020 at 14:33):

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

Bryan Gin-ge Chen (Jan 27 2020 at 16:29):

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 (Jan 27 2020 at 16:30):

We're working on the authentication thing.

Rob Lewis (Jan 27 2020 at 16:31):

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

Rob Lewis (Jan 27 2020 at 16:31):

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

Gabriel Ebner (Jan 28 2020 at 18:53):

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

Gabriel Ebner (Jan 28 2020 at 18:53):

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 (Jan 28 2020 at 18:54):

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 (Jan 28 2020 at 18:55):

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 (Jan 28 2020 at 19:00):

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

Rob Lewis (Jan 28 2020 at 19:01):

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 (Jan 28 2020 at 19:01):

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

Rob Lewis (Jan 28 2020 at 19:02):

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

Rob Lewis (Jan 28 2020 at 19:03):

Okay, yeah, I guess it sounds plausible.

Gabriel Ebner (Jan 28 2020 at 19:03):

I'm not sure either.

Rob Lewis (Jan 28 2020 at 19:05):

Well, fingers crossed once again.

Gabriel Ebner (Jan 28 2020 at 20:35):

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 (Jan 28 2020 at 20:38):

Done.

Gabriel Ebner (Jan 28 2020 at 20:38):

Thank you!

Rob Lewis (Jan 28 2020 at 20:38):

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

Gabriel Ebner (Jan 28 2020 at 20:39):

I've already fixed it.

Rob Lewis (Jan 28 2020 at 20:39):

Ah, cool.

Gabriel Ebner (Jan 28 2020 at 20:40):

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

Rob Lewis (Jan 28 2020 at 21:46):

:tada:

Rob Lewis (Jan 28 2020 at 21:46):

Thanks Gabriel!

Rob Lewis (Jan 30 2020 at 13:18):

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 (Jan 30 2020 at 13:58):

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 (Jan 30 2020 at 17:03):

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 (Jan 30 2020 at 19:01):

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

Rob Lewis (Jan 30 2020 at 20:28):

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

Rob Lewis (Feb 11 2020 at 11:14):

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 (Feb 18 2020 at 12:24):

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 (Feb 18 2020 at 12:35):

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

Rob Lewis (Feb 18 2020 at 12:36):

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 (Feb 18 2020 at 12:36):

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

Patrick Massot (Feb 18 2020 at 12:37):

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

Rob Lewis (Feb 18 2020 at 12:37):

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

Rob Lewis (Feb 18 2020 at 12:37):

Patrick Massot said:

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

Maybe, no idea.

Gabriel Ebner (Feb 18 2020 at 12:37):

Yeah, please go for it.

Patrick Massot (Feb 18 2020 at 12:40):

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 (Feb 18 2020 at 13:04):

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 (Feb 18 2020 at 13:10):

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

Patrick Massot (Feb 18 2020 at 13:11):

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

Bryan Gin-ge Chen (Feb 18 2020 at 13:17):

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

Bryan Gin-ge Chen (Feb 18 2020 at 13:19):

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 (Feb 18 2020 at 13:32):

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 (Feb 18 2020 at 13:32):

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

Patrick Massot (Feb 18 2020 at 13:34):

What is a PAT?

Rob Lewis (Feb 18 2020 at 13:37):

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

Patrick Massot (Feb 18 2020 at 13:38):

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

Jasmin Blanchette (Feb 18 2020 at 22:26):

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


Last updated: Dec 20 2023 at 11:08 UTC