build.yml

name: continuous integration

on:
  push:
    branches-ignore:
      # ignore tmp branches used by bors
      - 'staging.tmp*'
      - 'trying.tmp*'
      - 'staging*.tmp'
      # ignore staging and trying branches used by bors, these are handled by bors.yml
      - 'staging'
      - 'trying'
      # ignore branches meant for experiments
      - 'ci-dev/**'

concurrency:
  # label each workflow run; only the latest with each label will run
  # workflows on master get more expressive labels
  group: ${{ github.workflow }}-${{ github.ref }}-${{ (github.event_name == 'push' && github.ref == 'refs/heads/master' && github.run_id) || '' }}
  # cancel any running workflow with the same label
  cancel-in-progress: true

# Limit permissions for GITHUB_TOKEN for the entire workflow
permissions:
  contents: read
  id-token: write
  pull-requests: write  # Only allow PR comments/labels
  # All other permissions are implicitly 'none'

jobs:
  build:
    name: ci
    if: ${{ github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing' }}
    uses: ./.github/workflows/build_template.yml
    with:
      concurrency_group: ${{ github.workflow }}-${{ github.ref }}-${{ (github.event_name == 'push' && github.ref == 'refs/heads/master' && github.run_id) || '' }}
      pr_branch_ref: ${{ github.sha }}
      # Use the MASTER cache key only on mathlib4/master; nightly-testing and other branches use NON_MASTER
      cache_application_id: ${{ github.repository == 'leanprover-community/mathlib4' && github.ref == 'refs/heads/master' && vars.CACHE_MASTER_WRITER_AZURE_APP_ID || vars.CACHE_NON_MASTER_WRITER_AZURE_APP_ID }}
      runs_on: pr
    secrets: inherit