schedule.yml

name: Scheduled Update

on:
  schedule:
    # 9:00 AM EST / 10:00 AM EDT
    - cron: '00 14 * * 1,3,5'
    - cron: '00 14 * * 0,4'
    - cron: '00 14 * * 2,6'
  # Enable testing this workflow manually from the Actions tab
  workflow_dispatch:
    inputs:
      index-repo:
        description: "Registry index repository"
        type: string
        required: false
        default: leanprover/reservoir-index
      testbed-size:
        description: "Max number of testbed entries"
        type: number
        required: false
      testbed-toolchain:
        description: "Lean toolchain(s) on which to build"
        type: string
        required: true
        default: package
      dry-run:
        description: "Do not update site and index"
        type: boolean
        required: false
        default: false


# GITHUB_TOKEN permissions needed for deployment (copied from website.yml)
permissions:
  contents: read
  statuses: write

jobs:
  testbed:
    name: Testbed
    uses: ./.github/workflows/testbed.yml
    secrets: inherit
    with:
      index-repo: ${{ inputs.index-repo || 'leanprover/reservoir-index' }}
      search-packages: true
      package-pattern: ".*"
      toolchain: ${{ inputs.testbed-toolchain || github.event.schedule == '00 14 * * 1,3,5' && 'package' || github.event.schedule == '00 14 * * 0,4' && 'latest' || 'stable'}}
      max-size: ${{ toJson(inputs.testbed-size) == 'null' && -1 || fromJson(inputs.testbed-size) }}
      cache-builds: ${{ inputs.dry-run != 'true' }}
      update-index: ${{ inputs.dry-run != 'true' }}
  website:
    needs: [testbed]
    name: Website
    uses: ./.github/workflows/website.yml
    secrets: inherit
    with:
      index-repo: ${{ inputs.index-repo || 'leanprover/reservoir-index' }}
      production-deploy: ${{ inputs.dry-run != 'true' }}