ci.yml

name: CI

on:
  push:
    branches:
      - master
      - 'stage/**' # branch pattern for general changes
  pull_request:
    branches:
      - master
  # Enable running this workflow manually from the Actions tab
  workflow_dispatch:
    inputs:
      index:
        description: "What index to use"
        type: choice
        options:
          # Use the current state of the index repository (i.e., reservoir-index)
          - current
          # Update the index repository and then use it
          - updated
          # Create and use a small local index artifact (e.g., for testing)
          - local
        required: true
        default: current
      toolchain:
        description: "Lean toolchain to test against"
        type: string
        required: false
      testbed-size:
        description: "Number of packages to test"
        type: number
        required: false
      save-testbed:
        description: "Save testbed results to reservoir-index"
        type: boolean
        required: false
        default: true

# GITHUB_TOKEN permissions needed for deployment (copied from pages.yaml)
permissions:
  contents: read
  deployments: none
  pull-requests: write
  statuses: write

jobs:
  index:
    name: Index
    if: (!inputs.index || inputs.index != 'current')
    uses: ./.github/workflows/index.yaml
    secrets: inherit
    with:
      update-index: ${{ inputs.index == 'updated' }}
  testbed:
    needs: index
    # Run even if `index` is skipped
    if: (!failure() && !cancelled())
    name: Testbed
    uses: ./.github/workflows/testbed.yaml
    with:
      index-artifact: ${{ !inputs.index || inputs.index == 'local' }}
      toolchain: ${{ inputs.toolchain }}
      testbed-size: ${{ inputs.testbed-size }}
      update-index: ${{ inputs.save-testbed }}
  pages:
    needs: [index, testbed]
    # Run even if `index` is skipped
    if: (!failure() && !cancelled())
    name: Pages
    uses: ./.github/workflows/pages.yaml
    secrets: inherit
    with:
      index-artifact: ${{ !inputs.index || inputs.index == 'local' }}