Reservoir and CI

Stream: lean4

[Patrick Massot]

@Mac Malone in your plans to use reservoir to host build artifacts, did you think about the permissions issue? Currently Mathlib uses a very weird workflow where we very strongly encourage people to open PRs from branches of the main repo instead of forks, because we want CI to build PRs and we don't want that everyone can push to our olean server. Fixing this weirdness would be very nice.

[Mac Malone]

@Patrick Massot What kind of fix are you looking for here? To fix the specific issue you mentioned, one option (just with GitHub) would be to build the repository using a pull_request workflow, upload the build result as an artifact, and then spawn another workflow via workflow_run to download the artfiact and upload to it to olean server. As the workflow_run event always runs from the main repo's default branch, it could use a user whitelist to determine which build artifacts should be cached without being compromised by PRs from arbitrary users.

[Patrick Massot]

I don't know actually, I was never involved in this CI stuff, but I tried to reproduce the explanation of our weird workflow that CI aware people always give.

[Scott Morrison]

Mac's solution sounds pretty good to me, if someone wants to try it.

As a related example, I recently added a workflow_run job at Mathlib to post to zulip about the nightly-testing branch, and there are several examples of using this on the lean4 repo.