5cc9f6f9cb
Currently we create `lean-pr-testing-NNNN` branches at Mathlib automatically for each Lean PR. We don't automatically create one at Std; mostly simply because Std fails less often, so it has been okay to do this manually as needed. It is conceptually simpler, however, if this is done uniformly. This PR: * does not proceed with Std/Mathlib CI unless the appropriate `nightly-testing-YYYY-MM-DD` tag exists at Std (like it already doesn't proceed if that tag is missing at Mathlib) * creates `lean-pr-testing-NNNN` branches at Std * when it creates `lean-pr-testing-NNNN` branches at Mathlib, updates the Std dependency to use the `lean-pr-testing-NNNN` branch at Std - [x] depends on #3199 Note that because most users do not have write access at Std, in order to make updates to `lean-pr-testing-NNNN` branches there they will need to make PRs. These will be merged with a very low bar, and feel free to ping me for assistance on this. If this is annoying we will automate. Also, frequent contributors to Lean may ask @digama0 or @joehendrix for write access in order to easily work on these branches. This PR requires that we have a secret here with write access at Std. I'm arranging that [on zulip](https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/bot.20access/near/416686090). I will update the documentation at https://leanprover-community.github.io/contribute/tags_and_branches.html to reflect these changes when they are merged. --------- Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> |
||
|---|---|---|
| .. | ||
| actionlint.yml | ||
| backport.yml | ||
| ci.yml | ||
| labels-from-comments.yml | ||
| nix-ci.yml | ||
| pr-release.yml | ||
| pr-title.yml | ||
| stale.yml | ||
| update-stage0.yml | ||