Trigger CI for leanprover/lean4#5669

.github/workflows/build.yml

@@ -9,6 +9,10 @@ on:
 
 name: ci
 
+concurrency:
+  group: build-${{ github.sha }}
+  cancel-in-progress: true
+
 jobs:
   build:
     name: Build
@@ -54,4 +58,4 @@ jobs:
       - name: Don't 'import Lean', use precise imports
         if: always()
         run: |
-          ! (find . -name "*.lean" ! -path "./test/import_lean.lean" -type f -print0 | xargs -0 grep -E -n '^import Lean$')
+          ! (find . -name "*.lean" ! -path "./BatteriesTest/import_lean.lean" -type f -print0 | xargs -0 grep -E -n '^import Lean$')

.github/workflows/docs-deploy.yml

@@ -0,0 +1,38 @@
+name: Deploy Docs
+
+on:
+  workflow_dispatch:
+  schedule:
+    - cron: '0 10 * * *' # daily (UTC 10:00)
+
+permissions:
+  contents: write
+
+jobs:
+  deploy-docs:
+    runs-on: ubuntu-latest
+    if: github.repository_owner == 'leanprover-community'
+    steps:
+
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Install Lean
+        uses: leanprover/lean-action@v1
+        with:
+          test: false
+          lint: false
+          use-github-cache: true
+
+      - name: Build Docs
+        working-directory: docs
+        run: lake build --keep-toolchain -q Batteries:docs
+
+      - name: Deploy Docs
+        run: |
+          git config user.name "leanprover-community-batteries-bot"
+          git config user.email "[email protected]"
+          git checkout -b docs
+          git add docs/doc docs/doc-data
+          git commit -m "chore: generate docs"
+          git push origin docs --force

.github/workflows/docs-release.yml

@@ -0,0 +1,48 @@
+name: Release Docs
+
+on:
+  push:
+    tags:
+      - "v[0-9]+.[0-9]+.[0-9]+"
+      - "v[0-9]+.[0-9]+.[0-9]+-rc[0-9]+"
+
+permissions:
+  contents: write
+
+jobs:
+  build-docs:
+    runs-on: ubuntu-latest
+    if: github.repository_owner == 'leanprover-community'
+    steps:
+
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Install Lean
+        uses: leanprover/lean-action@v1
+        with:
+          test: false
+          lint: false
+          use-github-cache: true
+
+      - name: Build Docs
+        working-directory: docs
+        run: lake build --keep-toolchain -q Batteries:docs
+
+      - name: Compress Docs
+        working-directory: docs
+        env:
+          TAG_NAME: ${{ github.ref_name }}
+        run: |
+          tar -czf docs-${TAG_NAME}.tar.gz doc doc-data
+          zip -rq docs-${TAG_NAME}.zip doc doc-data
+
+      - name: Release Docs
+        uses: softprops/action-gh-release@v2
+        with:
+          prerelease: ${{ contains(github.ref, 'rc') }}
+          make_latest: ${{ !contains(github.ref, 'rc') }}
+          files: |
+            docs/docs-${{ github.ref_name }}.tar.gz
+            docs/docs-${{ github.ref_name }}.zip
+          fail_on_unmatched_files: true

.github/workflows/labels-from-status.yml

@@ -0,0 +1,65 @@
+# This workflow assigns `awaiting-review` or `WIP` labels to new PRs, and it removes
+# `awaiting-review`, `awaiting-author`, or `WIP` label from closed PRs.
+# It does not modify labels for open PRs that already have one of the `awaiting-review`,
+# `awaiting-author`, or `WIP` labels.
+
+name: Label PR from status change
+
+permissions:
+  contents: read
+  pull-requests: write
+
+on:
+  pull_request:
+    types:
+      - closed
+      - opened
+      - reopened
+      - converted_to_draft
+      - ready_for_review
+    branches:
+      - main
+
+jobs:
+  auto-label:
+    if: github.repository_owner == 'leanprover-community'
+    runs-on: ubuntu-latest
+    steps:
+
+    - uses: actions/checkout@v4
+      with:
+        fetch-depth: 0
+
+    - name: Unlabel closed PR
+      if: github.event.pull_request.state == 'closed'
+      uses: actions-ecosystem/action-remove-labels@v1
+      with:
+        github_token: ${{ secrets.GITHUB_TOKEN }}
+        labels: |
+          WIP
+          awaiting-author
+          awaiting-review
+
+    - name: Label unlabeled draft PR as WIP
+      if: |
+        github.event.pull_request.state == 'open' &&
+        github.event.pull_request.draft &&
+        ! contains(github.event.pull_request.labels.*.name, 'awaiting-author') &&
+        ! contains(github.event.pull_request.labels.*.name, 'awaiting-review') &&
+        ! contains(github.event.pull_request.labels.*.name, 'WIP')
+      uses: actions-ecosystem/action-add-labels@v1
+      with:
+        github_token: ${{ secrets.GITHUB_TOKEN }}
+        labels: WIP
+
+    - name: Label unlabeled other PR as awaiting-review
+      if: |
+        github.event.pull_request.state == 'open' &&
+        ! github.event.pull_request.draft &&
+        ! contains(github.event.pull_request.labels.*.name, 'awaiting-author') &&
+        ! contains(github.event.pull_request.labels.*.name, 'awaiting-review') &&
+        ! contains(github.event.pull_request.labels.*.name, 'WIP')
+      uses: actions-ecosystem/action-add-labels@v1
+      with:
+        github_token: ${{ secrets.GITHUB_TOKEN }}
+        labels: awaiting-review

.github/workflows/nightly_detect_failure.yml

@@ -44,6 +44,7 @@ jobs:
         toolchain=$(<lean-toolchain)
         if [[ $toolchain =~ leanprover/lean4:nightly-([a-zA-Z0-9_-]+) ]]; then
           version=${BASH_REMATCH[1]}
+          printf 'NIGHTLY=%s\n' "${version}" >> "${GITHUB_ENV}"
           if git ls-remote --tags --exit-code origin "refs/tags/nightly-testing-$version" >/dev/null; then
               echo "Tag nightly-testing-$version already exists on the remote."
           else
@@ -52,6 +53,8 @@ jobs:
               git tag nightly-testing-$version
               git push origin nightly-testing-$version
           fi
+          hash="$(git rev-parse "nightly-testing-${version}")"
+          printf 'SHA=%s\n' "${hash}" >> "${GITHUB_ENV}"
         else
           echo "Error: The file lean-toolchain does not contain the expected pattern."
           exit 1
@@ -63,9 +66,15 @@ jobs:
       run: pip install zulip
 
     - name: Check last message and post if necessary
+      env:
+        ZULIP_EMAIL: '[email protected]'
+        ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
+        ZULIP_SITE: 'https://leanprover.zulipchat.com'
+        SHA: ${{ env.SHA }}
       run: |
+        import os
         import zulip
-        client = zulip.Client(email='[email protected]', api_key='${{ secrets.ZULIP_API_KEY }}', site='https://leanprover.zulipchat.com')
+        client = zulip.Client(email=os.getenv('ZULIP_EMAIL'), api_key=os.getenv('ZULIP_API_KEY'), site=os.getenv('ZULIP_SITE'))
 
         # Get the last message in the 'status updates' topic
         request = {
@@ -77,14 +86,146 @@ jobs:
         }
         response = client.get_messages(request)
         messages = response['messages']
-        if not messages or messages[0]['content'] != "✅️ The latest CI for Batteries' [`nightly-testing`](https://github.com/leanprover-community/batteries/tree/nightly-testing) branch has succeeded!":
+        if not messages or messages[0]['content'] != f"✅️ The latest CI for Batteries' [`nightly-testing`](https://github.com/leanprover-community/batteries/tree/nightly-testing) branch has succeeded! ([{os.getenv('SHA')}](https://github.com/${{ github.repository }}/commit/{os.getenv('SHA')}))":
             # Post the success message
             request = {
                 'type': 'stream',
                 'to': 'nightly-testing',
                 'topic': 'Batteries status updates',
-                'content': "✅️ The latest CI for Batteries' [`nightly-testing`](https://github.com/leanprover-community/batteries/tree/nightly-testing) branch has succeeded!"
+                'content': f"✅️ The latest CI for Batteries' [`nightly-testing`](https://github.com/leanprover-community/batteries/tree/nightly-testing) branch has succeeded! ([{os.getenv('SHA')}](https://github.com/${{ github.repository }}/commit/{os.getenv('SHA')}))"
             }
             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: Send warning message on Zulip if pattern doesn't match
+      if: failure()
+      uses: zulip/github-actions-zulip/send-message@v1
+      with:
+        api-key: ${{ secrets.ZULIP_API_KEY }}
+        email: '[email protected]'
+        organization-url: 'https://leanprover.zulipchat.com'
+        to: 'nightly-testing'
+        type: 'stream'
+        topic: 'Batteries status updates'
+        content: |
+          ⚠️ Warning: The lean-toolchain file in the latest bump branch does not match the expected pattern 'leanprover/lean4:nightly-YYYY-MM-DD'.
+          Current content: ${{ steps.bump_version.outputs.toolchain_content }}
+          This needs to be fixed for the nightly testing process to work correctly.
+
+    - 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 Batteries 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.')