name: Daily CI Workflow
# This workflow runs daily on `master` and the latest `nightly-testing-YYYY-MM-DD` tag,
# running some expensive CI checks that we don't want to run on every PR.
# It reports results via Zulip.

# This script requires that the ZULIP_API_KEY secret is available in both
# `leanprover-community/mathlib4` and `leanprover-community/mathlib4-nightly-testing`
# repositories.

on:
  schedule:
    - cron: '0 0 * * *'   # Runs at 00:00 UTC every day
  workflow_dispatch:

env:
  DEFAULT_BRANCH: master
  TAG_PATTERN: '^nightly-testing-[0-9]{4}-[0-9]{2}-[0-9]{2}$'

permissions:
  contents: read
  actions: read

jobs:
  check-leanchecker:
    runs-on: ubuntu-latest
    if: github.repository == 'leanprover-community/mathlib4'
    strategy:
      fail-fast: false
      matrix:
        branch_type: [master, nightly]
    steps:
      # Checkout repository, so that we can fetch tags to decide which branch we want.
      - name: Checkout branch or tag
        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1

      - name: Fetch latest tags (if nightly)
        if: matrix.branch_type == 'nightly'
        run: |
          # When in nightly mode, fetch tags from the nightly-testing repository
          git remote add nightly-testing https://github.com/leanprover-community/mathlib4-nightly-testing.git
          git fetch nightly-testing --tags
          LATEST_TAG=$(git tag | grep -E "${{ env.TAG_PATTERN }}" | sort -r | head -n 1)
          echo "LATEST_TAG=${LATEST_TAG}" >> "$GITHUB_ENV"

      - name: Set branch ref
        run: |
          if [ "${{ matrix.branch_type }}" == "master" ]; then
            echo "BRANCH_REF=${{ env.DEFAULT_BRANCH }}" >> "$GITHUB_ENV"
          else
            echo "BRANCH_REF=${{ env.LATEST_TAG }}" >> "$GITHUB_ENV"
          fi

      # Checkout the branch or tag we want to test.
      - name: Checkout branch or tag
        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
        with:
          repository: ${{ matrix.branch_type == 'nightly' && 'leanprover-community/mathlib4-nightly-testing' || github.repository }}
          ref: ${{ env.BRANCH_REF }}

      - name: Configure Lean
        uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5.0
        with:
          auto-config: false
          use-github-cache: false
          use-mathlib-cache: true
          reinstall-transient-toolchain: true

      - name: Check environments using leanchecker # make sure this name is consistent with "Get job status and URLs" in the notify job
        id: leanchecker
        run: |
          # `--fresh` is safe and in fact currently faster for projects with many modules
          lake env leanchecker --fresh Mathlib
          lake env leanchecker --fresh Batteries

  notify-leanchecker:
    runs-on: ubuntu-latest
    needs: check-leanchecker
    if: github.repository == 'leanprover-community/mathlib4' && always()
    strategy:
      fail-fast: false
      matrix:
        branch_type: [master, nightly]
    steps:
      - name: Checkout repository
        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1

      - name: Get job status and URLs
        id: get-status
        env:
          GH_TOKEN: ${{ github.token }}
        run: |
          JOB_NAME="check-leanchecker (${{ matrix.branch_type }})"

          # Get URL and conclusion for the specific job
          JOB_DATA=$(gh run view ${{ github.run_id }} --json jobs --jq \
            ".jobs[] | select(.name == \"$JOB_NAME\")")

          LEANCHECKER_URL=$(echo "$JOB_DATA" | jq -r \
            '(.url + (.steps[] | select(.name == "Check environments using leanchecker")
            | "#step:\(.number):1"))')

          JOB_CONCLUSION=$(echo "$JOB_DATA" | jq -r '.conclusion')

          echo "leanchecker_url=${LEANCHECKER_URL}" | tee -a "$GITHUB_OUTPUT"
          echo "job_conclusion=${JOB_CONCLUSION}" | tee -a "$GITHUB_OUTPUT"

      - name: Fetch latest tags (if nightly)
        if: matrix.branch_type == 'nightly'
        run: |
          git remote add nightly-testing https://github.com/leanprover-community/mathlib4-nightly-testing.git
          git fetch nightly-testing --tags
          LATEST_TAG=$(git tag | grep -E "${{ env.TAG_PATTERN }}" | sort -r | head -n 1)
          echo "LATEST_TAG=${LATEST_TAG}" | tee -a "$GITHUB_ENV"

      - name: Set branch ref
        run: |
          if [ "${{ matrix.branch_type }}" == "master" ]; then
            echo "BRANCH_REF=${{ env.DEFAULT_BRANCH }}" >> "$GITHUB_ENV"
          else
            echo "BRANCH_REF=${{ env.LATEST_TAG }}" >> "$GITHUB_ENV"
          fi

      - name: Identify the commit that was tested
        run: |
          if [ "${{ matrix.branch_type }}" == "master" ]; then
            echo "TESTED_REPO=${{ github.repository }}" >> "$GITHUB_ENV"
            echo "TESTED_SHA=${{ github.sha }}" >> "$GITHUB_ENV"
          else
            # `github.sha` is this workflow's own checkout of `master`, not the commit the
            # `nightly` leg tested, so resolve the tag that leg actually checked out.
            echo "TESTED_REPO=leanprover-community/mathlib4-nightly-testing" >> "$GITHUB_ENV"
            echo "TESTED_SHA=$(git rev-parse "${LATEST_TAG}^{commit}")" >> "$GITHUB_ENV"
          fi

      - name: Post success message for leanchecker on Zulip
        if: steps.get-status.outputs.job_conclusion == 'success'
        uses: zulip/github-actions-zulip/send-message@f675f2b4eb2a95fae974215476dcb7ad8dfeff6b # v2.0.2
        with:
          api-key: ${{ secrets.ZULIP_API_KEY }}
          email: 'github-mathlib4-bot@leanprover.zulipchat.com'
          organization-url: 'https://leanprover.zulipchat.com'
          to: 'nightly-testing-mathlib'
          type: 'stream'
          topic: 'leanchecker'
          content: |
            ✅ leanchecker [succeeded](${{ steps.get-status.outputs.leanchecker_url }}) on ${{ env.TESTED_REPO }}@${{ env.TESTED_SHA }} (ref: ${{ env.BRANCH_REF }})

      - name: Post failure / cancelled message for leanchecker on Zulip
        if: steps.get-status.outputs.job_conclusion != 'success'
        uses: zulip/github-actions-zulip/send-message@f675f2b4eb2a95fae974215476dcb7ad8dfeff6b # v2.0.2
        with:
          api-key: ${{ secrets.ZULIP_API_KEY }}
          email: 'github-mathlib4-bot@leanprover.zulipchat.com'
          organization-url: 'https://leanprover.zulipchat.com'
          to: 'nightly-testing-mathlib'
          type: 'stream'
          topic: 'leanchecker failure'
          content: |
            ❌ leanchecker [${{ steps.get-status.outputs.job_conclusion }}](${{ steps.get-status.outputs.leanchecker_url }}) on ${{ env.TESTED_REPO }}@${{ env.TESTED_SHA }} (ref: ${{ env.BRANCH_REF }})

  check-mathlib_test_executable:
    runs-on: ubuntu-latest
    if: github.repository == 'leanprover-community/mathlib4'
    strategy:
      fail-fast: false
      matrix:
        branch_type: [master, nightly]
    steps:
      # Checkout repository, so that we can fetch tags to decide which branch we want.
      - name: Checkout branch or tag
        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1

      - name: Fetch latest tags (if nightly)
        if: matrix.branch_type == 'nightly'
        run: |
          # When in nightly mode, fetch tags from the nightly-testing repository
          git remote add nightly-testing https://github.com/leanprover-community/mathlib4-nightly-testing.git
          git fetch nightly-testing --tags
          LATEST_TAG=$(git tag | grep -E "${{ env.TAG_PATTERN }}" | sort -r | head -n 1)
          echo "LATEST_TAG=${LATEST_TAG}" >> "$GITHUB_ENV"

      - name: Set branch ref
        run: |
          if [ "${{ matrix.branch_type }}" == "master" ]; then
            echo "BRANCH_REF=${{ env.DEFAULT_BRANCH }}" >> "$GITHUB_ENV"
          else
            echo "BRANCH_REF=${{ env.LATEST_TAG }}" >> "$GITHUB_ENV"
          fi

      # Checkout the branch or tag we want to test.
      - name: Checkout branch or tag
        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
        with:
          repository: ${{ matrix.branch_type == 'nightly' && 'leanprover-community/mathlib4-nightly-testing' || github.repository }}
          ref: ${{ env.BRANCH_REF }}

      - name: Configure Lean
        uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5.0
        with:
          auto-config: false
          use-github-cache: false
          use-mathlib-cache: true
          reinstall-transient-toolchain: true

      - name: Run mathlib_test_executable # make sure this name is consistent with "Get job status and URLs" in the notify job
        id: mathlib-test
        run: |
          lake exe mathlib_test_executable

  notify-mathlib_test_executable:
    runs-on: ubuntu-latest
    needs: check-mathlib_test_executable
    if: github.repository == 'leanprover-community/mathlib4' && always()
    strategy:
      fail-fast: false
      matrix:
        branch_type: [master, nightly]
    steps:
      - name: Checkout repository
        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1

      - name: Get job status and URLs
        id: get-status
        env:
          GH_TOKEN: ${{ github.token }}
        run: |
          JOB_NAME="check-mathlib_test_executable (${{ matrix.branch_type }})"

          # Get URL and conclusion for the specific job
          JOB_DATA=$(gh run view ${{ github.run_id }} --json jobs --jq \
            ".jobs[] | select(.name == \"$JOB_NAME\")")

          MATHLIB_TEST_EXECUTABLE_URL=$(echo "$JOB_DATA" | jq -r \
            '(.url + (.steps[] | select(.name == "Run mathlib_test_executable")
            | "#step:\(.number):1"))')

          JOB_CONCLUSION=$(echo "$JOB_DATA" | jq -r '.conclusion')

          echo "mathlib_test_executable_url=${MATHLIB_TEST_EXECUTABLE_URL}" | tee -a "$GITHUB_OUTPUT"
          echo "job_conclusion=${JOB_CONCLUSION}" | tee -a "$GITHUB_OUTPUT"

      - name: Fetch latest tags (if nightly)
        if: matrix.branch_type == 'nightly'
        run: |
          git remote add nightly-testing https://github.com/leanprover-community/mathlib4-nightly-testing.git
          git fetch nightly-testing --tags
          LATEST_TAG=$(git tag | grep -E "${{ env.TAG_PATTERN }}" | sort -r | head -n 1)
          echo "LATEST_TAG=${LATEST_TAG}" | tee -a "$GITHUB_ENV"

      - name: Set branch ref
        run: |
          if [ "${{ matrix.branch_type }}" == "master" ]; then
            echo "BRANCH_REF=${{ env.DEFAULT_BRANCH }}" >> "$GITHUB_ENV"
          else
            echo "BRANCH_REF=${{ env.LATEST_TAG }}" >> "$GITHUB_ENV"
          fi

      - name: Identify the commit that was tested
        run: |
          if [ "${{ matrix.branch_type }}" == "master" ]; then
            echo "TESTED_REPO=${{ github.repository }}" >> "$GITHUB_ENV"
            echo "TESTED_SHA=${{ github.sha }}" >> "$GITHUB_ENV"
          else
            # `github.sha` is this workflow's own checkout of `master`, not the commit the
            # `nightly` leg tested, so resolve the tag that leg actually checked out.
            echo "TESTED_REPO=leanprover-community/mathlib4-nightly-testing" >> "$GITHUB_ENV"
            echo "TESTED_SHA=$(git rev-parse "${LATEST_TAG}^{commit}")" >> "$GITHUB_ENV"
          fi

      - name: Post success message for mathlib_test_executable on Zulip
        if: steps.get-status.outputs.job_conclusion == 'success'
        uses: zulip/github-actions-zulip/send-message@f675f2b4eb2a95fae974215476dcb7ad8dfeff6b # v2.0.2
        with:
          api-key: ${{ secrets.ZULIP_API_KEY }}
          email: 'github-mathlib4-bot@leanprover.zulipchat.com'
          organization-url: 'https://leanprover.zulipchat.com'
          to: 'nightly-testing-mathlib'
          type: 'stream'
          topic: 'mathlib test executable'
          content: |
            ✅ mathlib_test_executable [succeeded](${{ steps.get-status.outputs.mathlib_test_executable_url }}) on ${{ env.TESTED_REPO }}@${{ env.TESTED_SHA }} (ref: ${{ env.BRANCH_REF }})

      - name: Post failure / cancelled message for mathlib_test_executable on Zulip
        if: steps.get-status.outputs.job_conclusion != 'success'
        uses: zulip/github-actions-zulip/send-message@f675f2b4eb2a95fae974215476dcb7ad8dfeff6b # v2.0.2
        with:
          api-key: ${{ secrets.ZULIP_API_KEY }}
          email: 'github-mathlib4-bot@leanprover.zulipchat.com'
          organization-url: 'https://leanprover.zulipchat.com'
          to: 'nightly-testing-mathlib'
          type: 'stream'
          topic: 'mathlib test executable failure'
          content: |
            ❌ mathlib_test_executable [${{ steps.get-status.outputs.job_conclusion }}](${{ steps.get-status.outputs.mathlib_test_executable_url }}) on ${{ env.TESTED_REPO }}@${{ env.TESTED_SHA }} (ref: ${{ env.BRANCH_REF }})

  check-nanoda:
    runs-on: ubuntu-latest
    if: github.repository == 'leanprover-community/mathlib4'
    strategy:
      fail-fast: false
      matrix:
        branch_type: [master, nightly]
    steps:
      # Checkout repository, so that we can fetch tags to decide which branch we want.
      - name: Checkout branch or tag
        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1

      - name: Fetch latest tags (if nightly)
        if: matrix.branch_type == 'nightly'
        run: |
          # When in nightly mode, fetch tags from the nightly-testing repository
          git remote add nightly-testing https://github.com/leanprover-community/mathlib4-nightly-testing.git
          git fetch nightly-testing --tags
          LATEST_TAG=$(git tag | grep -E "${{ env.TAG_PATTERN }}" | sort -r | head -n 1)
          echo "LATEST_TAG=${LATEST_TAG}" >> "$GITHUB_ENV"

      - name: Set branch ref
        run: |
          if [ "${{ matrix.branch_type }}" == "master" ]; then
            echo "BRANCH_REF=${{ env.DEFAULT_BRANCH }}" >> "$GITHUB_ENV"
          else
            echo "BRANCH_REF=${{ env.LATEST_TAG }}" >> "$GITHUB_ENV"
          fi

      # Checkout the branch or tag we want to test.
      - name: Checkout branch or tag
        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
        with:
          repository: ${{ matrix.branch_type == 'nightly' && 'leanprover-community/mathlib4-nightly-testing' || github.repository }}
          ref: ${{ env.BRANCH_REF }}

      - name: Configure Lean
        uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5.0
        with:
          auto-config: false
          use-github-cache: false
          use-mathlib-cache: true
          reinstall-transient-toolchain: true

      - name: Install Rust
        uses: dtolnay/rust-toolchain@631a55b12751854ce901bb631d5902ceb48146f7 # stable

      - name: Check Mathlib using nanoda # make sure this name is consistent with "Get job status and URLs" in the notify job
        id: nanoda
        run: |
          # Clone and build lean4export
          # TODO: Once https://github.com/leanprover/lean4export/pull/11 is merged,
          # switch to leanprover/lean4export and remove the `git checkout` line below.
          git clone https://github.com/kim-em/lean4export
          cd lean4export
          git checkout fix-nondep-normalization
          # Match toolchain to mathlib
          cp ../lean-toolchain .
          lake build
          cd ..

          # Clone and build nanoda_lib
          git clone https://github.com/ammkrn/nanoda_lib
          cd nanoda_lib
          git checkout debug
          cargo build --release
          cd ..

          # Export Mathlib
          lake env lean4export/.lake/build/bin/lean4export Mathlib > mathlib_export.txt

          # Create config
          cat > nanoda_config.json << 'EOF'
          {
              "export_file_path": "mathlib_export.txt",
              "permitted_axioms": [
                  "propext",
                  "Classical.choice",
                  "Quot.sound",
                  "Lean.trustCompiler"
              ],
              "unpermitted_axiom_hard_error": false,
              "nat_extension": true,
              "string_extension": true,
              "print_success_message": true
          }
          EOF

          # Run nanoda
          nanoda_lib/target/release/nanoda_bin nanoda_config.json

  notify-nanoda:
    runs-on: ubuntu-latest
    needs: check-nanoda
    if: github.repository == 'leanprover-community/mathlib4' && always()
    strategy:
      fail-fast: false
      matrix:
        branch_type: [master, nightly]
    steps:
      - name: Checkout repository
        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1

      - name: Get job status and URLs
        id: get-status
        env:
          GH_TOKEN: ${{ github.token }}
        run: |
          JOB_NAME="check-nanoda (${{ matrix.branch_type }})"

          # Get URL and conclusion for the specific job
          JOB_DATA=$(gh run view ${{ github.run_id }} --json jobs --jq \
            ".jobs[] | select(.name == \"$JOB_NAME\")")

          NANODA_URL=$(echo "$JOB_DATA" | jq -r \
            '(.url + (.steps[] | select(.name == "Check Mathlib using nanoda")
            | "#step:\(.number):1"))')

          JOB_CONCLUSION=$(echo "$JOB_DATA" | jq -r '.conclusion')

          echo "nanoda_url=${NANODA_URL}" | tee -a "$GITHUB_OUTPUT"
          echo "job_conclusion=${JOB_CONCLUSION}" | tee -a "$GITHUB_OUTPUT"

      - name: Fetch latest tags (if nightly)
        if: matrix.branch_type == 'nightly'
        run: |
          git remote add nightly-testing https://github.com/leanprover-community/mathlib4-nightly-testing.git
          git fetch nightly-testing --tags
          LATEST_TAG=$(git tag | grep -E "${{ env.TAG_PATTERN }}" | sort -r | head -n 1)
          echo "LATEST_TAG=${LATEST_TAG}" | tee -a "$GITHUB_ENV"

      - name: Set branch ref
        run: |
          if [ "${{ matrix.branch_type }}" == "master" ]; then
            echo "BRANCH_REF=${{ env.DEFAULT_BRANCH }}" >> "$GITHUB_ENV"
          else
            echo "BRANCH_REF=${{ env.LATEST_TAG }}" >> "$GITHUB_ENV"
          fi

      - name: Identify the commit that was tested
        run: |
          if [ "${{ matrix.branch_type }}" == "master" ]; then
            echo "TESTED_REPO=${{ github.repository }}" >> "$GITHUB_ENV"
            echo "TESTED_SHA=${{ github.sha }}" >> "$GITHUB_ENV"
          else
            # `github.sha` is this workflow's own checkout of `master`, not the commit the
            # `nightly` leg tested, so resolve the tag that leg actually checked out.
            echo "TESTED_REPO=leanprover-community/mathlib4-nightly-testing" >> "$GITHUB_ENV"
            echo "TESTED_SHA=$(git rev-parse "${LATEST_TAG}^{commit}")" >> "$GITHUB_ENV"
          fi

      - name: Post success message for nanoda on Zulip
        if: steps.get-status.outputs.job_conclusion == 'success'
        uses: zulip/github-actions-zulip/send-message@f675f2b4eb2a95fae974215476dcb7ad8dfeff6b # v2.0.2
        with:
          api-key: ${{ secrets.ZULIP_API_KEY }}
          email: 'github-mathlib4-bot@leanprover.zulipchat.com'
          organization-url: 'https://leanprover.zulipchat.com'
          to: 'nightly-testing-mathlib'
          type: 'stream'
          topic: 'nanoda'
          content: |
            ✅ nanoda [succeeded](${{ steps.get-status.outputs.nanoda_url }}) on ${{ env.TESTED_REPO }}@${{ env.TESTED_SHA }} (ref: ${{ env.BRANCH_REF }})

      - name: Post failure / cancelled message for nanoda on Zulip
        if: steps.get-status.outputs.job_conclusion != 'success'
        uses: zulip/github-actions-zulip/send-message@f675f2b4eb2a95fae974215476dcb7ad8dfeff6b # v2.0.2
        with:
          api-key: ${{ secrets.ZULIP_API_KEY }}
          email: 'github-mathlib4-bot@leanprover.zulipchat.com'
          organization-url: 'https://leanprover.zulipchat.com'
          to: 'nightly-testing-mathlib'
          type: 'stream'
          topic: 'nanoda failure'
          content: |
            ❌ nanoda [${{ steps.get-status.outputs.job_conclusion }}](${{ steps.get-status.outputs.nanoda_url }}) on ${{ env.TESTED_REPO }}@${{ env.TESTED_SHA }} (ref: ${{ env.BRANCH_REF }})