-
Notifications
You must be signed in to change notification settings - Fork 110
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Trigger CI for leanprover/lean4#6261
- Loading branch information
Showing
52 changed files
with
1,498 additions
and
608 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -88,3 +88,120 @@ jobs: | |
| result = client.send_message(request) | ||
| print(result) | ||
| shell: python | ||
|
|
||
| # Next, determine if we should remind the humans to create a new PR to the `bump/v4.X.0` branch. | ||
|
|
||
| - name: Check for matching bump/nightly-YYYY-MM-DD branch | ||
| id: check_branch | ||
| uses: actions/github-script@v7 | ||
| with: | ||
| script: | | ||
| const branchName = `bump/nightly-${process.env.NIGHTLY}`; | ||
| const branches = await github.rest.repos.listBranches({ | ||
| owner: context.repo.owner, | ||
| repo: context.repo.repo | ||
| }); | ||
| const exists = branches.data.some(branch => branch.name === branchName); | ||
| if (exists) { | ||
| console.log(`Branch ${branchName} exists.`); | ||
| return true; | ||
| } else { | ||
| console.log(`Branch ${branchName} does not exist.`); | ||
| return false; | ||
| } | ||
| result-encoding: string | ||
|
|
||
| - name: Exit if matching branch exists | ||
| if: steps.check_branch.outputs.result == 'true' | ||
| run: | | ||
| echo "Matching bump/nightly-YYYY-MM-DD branch found, no further action needed." | ||
| exit 0 | ||
| - name: Fetch latest bump branch name | ||
| id: latest_bump_branch | ||
| uses: actions/github-script@v7 | ||
| with: | ||
| script: | | ||
| const branches = await github.paginate(github.rest.repos.listBranches, { | ||
| owner: context.repo.owner, | ||
| repo: context.repo.repo | ||
| }); | ||
| const bumpBranches = branches | ||
| .map(branch => branch.name) | ||
| .filter(name => name.match(/^bump\/v4\.\d+\.0$/)) | ||
| .sort((a, b) => b.localeCompare(a, undefined, {numeric: true, sensitivity: 'base'})); | ||
| if (!bumpBranches.length) { | ||
| throw new Exception("Did not find any bump/v4.x.0 branch") | ||
| } | ||
| const latestBranch = bumpBranches[0]; | ||
| return latestBranch; | ||
| - name: Fetch lean-toolchain from latest bump branch | ||
| id: bump_version | ||
| uses: actions/github-script@v7 | ||
| with: | ||
| script: | | ||
| const response = await github.rest.repos.getContent({ | ||
| owner: context.repo.owner, | ||
| repo: context.repo.repo, | ||
| path: 'lean-toolchain', | ||
| ref: ${{ steps.latest_bump_branch.outputs.result }} | ||
| }); | ||
| const content = Buffer.from(response.data.content, 'base64').toString(); | ||
| const version = content.match(/leanprover\/lean4:nightly-(\d{4}-\d{2}-\d{2})/)[1]; | ||
| return version; | ||
| - name: Compare versions and post a reminder. | ||
| env: | ||
| BUMP_VERSION: ${{ steps.bump_version.outputs.result }} | ||
| BUMP_BRANCH: ${{ steps.latest_bump_branch.outputs.result }} | ||
| SHA: ${{ env.SHA }} | ||
| ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }} | ||
| shell: python | ||
| run: | | ||
| import os | ||
| import zulip | ||
| client = zulip.Client(email='[email protected]', api_key=os.getenv('ZULIP_API_KEY'), site='https://leanprover.zulipchat.com') | ||
| current_version = os.getenv('NIGHTLY') | ||
| bump_version = os.getenv('BUMP_VERSION') | ||
| bump_branch = os.getenv('BUMP_BRANCH') | ||
| sha = os.getenv('SHA') | ||
| print(f'Current version: {current_version}, Bump version: {bump_version}, SHA: {sha}') | ||
| if current_version > bump_version: | ||
| print('Lean toolchain in `nightly-testing` is ahead of the bump branch.') | ||
| # Get the last message in the 'Batteries bump branch reminders' topic | ||
| request = { | ||
| 'anchor': 'newest', | ||
| 'num_before': 1, | ||
| 'num_after': 0, | ||
| 'narrow': [{'operator': 'stream', 'operand': 'nightly-testing'}, {'operator': 'topic', 'operand': 'Batteries bump branch reminders'}], | ||
| 'apply_markdown': False # Otherwise the content test below fails. | ||
| } | ||
| response = client.get_messages(request) | ||
| messages = response['messages'] | ||
| bump_branch_suffix = bump_branch.replace('bump/', '') | ||
| payload = f"🛠️: it looks like it's time to create a new bump/nightly-{current_version} branch from nightly-testing (specifically {sha}), and then PR that to {bump_branch}. " | ||
| payload += "To do so semi-automatically, run the following script from mathlib root:\n\n" | ||
| payload += f"```bash\n./scripts/create-adaptation-pr.sh --bumpversion={bump_branch_suffix} --nightlydate={current_version} --nightlysha={sha}\n```\n" | ||
| # Only post if the message is different | ||
| # We compare the first 160 characters, since that includes the date and bump version | ||
| if not messages or messages[0]['content'][:160] != payload[:160]: | ||
| # Log messages, because the bot seems to repeat itself... | ||
| if messages: | ||
| print("###### Last message:") | ||
| print(messages[0]['content']) | ||
| print("###### Current message:") | ||
| print(payload) | ||
| else: | ||
| print('The strings match!') | ||
| # Post the reminder message | ||
| request = { | ||
| 'type': 'stream', | ||
| 'to': 'nightly-testing', | ||
| 'topic': 'Batteries bump branch reminders', | ||
| 'content': payload | ||
| } | ||
| result = client.send_message(request) | ||
| print(result) | ||
| else: | ||
| print('No action needed.') | ||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,2 +1,4 @@ | ||
| import Batteries.Data.Fin.Basic | ||
| import Batteries.Data.Fin.Fold | ||
| import Batteries.Data.Fin.Lemmas | ||
| import Batteries.Data.Fin.OfBits |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,16 +1,19 @@ | ||
| /- | ||
| Copyright (c) 2017 Robert Y. Lewis. All rights reserved. | ||
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: Robert Y. Lewis, Keeley Hoek, Mario Carneiro | ||
| Authors: Robert Y. Lewis, Keeley Hoek, Mario Carneiro, François G. Dorais, Quang Dao | ||
| -/ | ||
| import Batteries.Tactic.Alias | ||
| import Batteries.Data.Array.Basic | ||
| import Batteries.Data.List.Basic | ||
|
|
||
| namespace Fin | ||
|
|
||
| /-- `min n m` as an element of `Fin (m + 1)` -/ | ||
| def clamp (n m : Nat) : Fin (m + 1) := ⟨min n m, Nat.lt_succ_of_le (Nat.min_le_right ..)⟩ | ||
|
|
||
| /-- `enum n` is the array of all elements of `Fin n` in order -/ | ||
| def enum (n) : Array (Fin n) := Array.ofFn id | ||
| @[deprecated (since := "2024-11-15")] | ||
| alias enum := Array.finRange | ||
|
|
||
| /-- `list n` is the list of all elements of `Fin n` in order -/ | ||
| def list (n) : List (Fin n) := (enum n).toList |
Oops, something went wrong.