feat: expand cache to full index #484
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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-repo: | |
| description: "Registry index repository" | |
| type: string | |
| required: false | |
| default: leanprover/reservoir-index | |
| search-packages: | |
| description: "Search GitHub for new packages" | |
| type: boolean | |
| required: false | |
| default: false | |
| package-pattern: | |
| description: "Regex search for indexed packages" | |
| type: string | |
| required: false | |
| default: ".*" | |
| version-pattern: | |
| description: "Regex search for version tags to build" | |
| type: string | |
| required: false | |
| testbed-toolchain: | |
| description: "Lean toolchain(s) on which to build" | |
| type: string | |
| required: true | |
| default: package | |
| testbed-size: | |
| description: "Max number of testbed entries" | |
| type: number | |
| required: false | |
| cache-builds: | |
| description: "Upload builds to cloud cache" | |
| type: boolean | |
| required: false | |
| update-index: | |
| description: "Save testbed results to index" | |
| type: boolean | |
| required: false | |
| production-deploy: | |
| description: "Deploy website to production" | |
| type: boolean | |
| required: false | |
| # GITHUB_TOKEN permissions needed for deployment (copied from website.yml) | |
| permissions: | |
| contents: read | |
| statuses: write | |
| # Permit only 1 concurrent run per branch when triggered automatically, cancelling previous ones. | |
| concurrency: | |
| group: ci/${{ github.event_name == 'workflow_dispatch' && github.run_id || github.ref_name }} | |
| cancel-in-progress: true | |
| jobs: | |
| config: | |
| name: Configure | |
| runs-on: ubuntu-latest | |
| outputs: | |
| index-repo: ${{ steps.compute.outputs.index-repo }} | |
| search-packages: ${{ steps.compute.outputs.search-packages }} | |
| update-index: ${{ steps.compute.outputs.update-index }} | |
| testbed: ${{ steps.compute.outputs.testbed }} | |
| package-pattern: ${{ steps.compute.outputs.package-pattern }} | |
| testbed-size: ${{ steps.compute.outputs.testbed-size }} | |
| testbed-toolchain: ${{ steps.compute.outputs.testbed-toolchain }} | |
| cache-builds: ${{ steps.compute.outputs.cache-builds }} | |
| production-deploy: ${{ steps.compute.outputs.production-deploy }} | |
| steps: | |
| # We echo even simple values out to make failures easier to debug from the logs | |
| - id: compute | |
| name: Compute Configuration | |
| run: | | |
| if ${{ github.event_name == 'pull_request' }}; then | |
| if ${{ contains(github.event.pull_request.labels.*.name, 'A-index') || contains(github.event.pull_request.labels.*.name, 'A-cache') }}; then | |
| echo testbed=true >> "$GITHUB_OUTPUT" | |
| echo 'package-pattern=.*' >> "$GITHUB_OUTPUT" | |
| elif ${{ contains(github.event.pull_request.labels.*.name, 'A-testbed') }}; then | |
| echo testbed=true >> "$GITHUB_OUTPUT" | |
| echo 'package-pattern=^leanprover' >> "$GITHUB_OUTPUT" | |
| fi | |
| echo search-packages=${{ contains(github.event.pull_request.labels.*.name, 'A-search') }} >> "$GITHUB_OUTPUT" | |
| echo 'testbed-toolchain=${{ (contains(github.event.pull_request.labels.*.name, 'A-testbed') || contains(github.event.pull_request.labels.*.name, 'A-cache')) && 'package,latest' || 'none' }}' >> "$GITHUB_OUTPUT" | |
| echo cache-builds=${{ contains(github.event.pull_request.labels.*.name, 'A-cache') }} >> "$GITHUB_OUTPUT" | |
| else | |
| if ${{ github.event_name == 'push' && github.ref_name == 'master' && contains(github.event.head_commit.message, 'UPDATE-INDEX') }}; then | |
| echo search-packages=false >> "$GITHUB_OUTPUT" | |
| echo update-index=true >> "$GITHUB_OUTPUT" | |
| echo testbed=true >> "$GITHUB_OUTPUT" | |
| echo 'package-pattern=.*' >> "$GITHUB_OUTPUT" | |
| echo testbed-toolchain=none >> "$GITHUB_OUTPUT" | |
| echo cache-builds=true >> "$GITHUB_OUTPUT" | |
| else | |
| if ${{ github.event_name != 'workflow_dispatch' }}; then | |
| echo testbed=${{ github.ref_name != 'master' }} >> "$GITHUB_OUTPUT" | |
| echo 'package-pattern=^leanprover' >> "$GITHUB_OUTPUT" | |
| else | |
| echo testbed=${{ toJson(inputs.testbed-size) == 'null' && true || inputs.testbed-size != 0 }} >> "$GITHUB_OUTPUT" | |
| echo 'package-pattern=${{ inputs.package-pattern }}' >> "$GITHUB_OUTPUT" | |
| fi | |
| echo search-packages=${{ inputs.search-packages == true }} >> "$GITHUB_OUTPUT" | |
| echo cache-builds=${{ inputs.cache-builds == true }} >> "$GITHUB_OUTPUT" | |
| echo update-index=${{ inputs.update-index == true }} >> "$GITHUB_OUTPUT" | |
| echo 'testbed-toolchain=${{ inputs.testbed-toolchain || 'none' }}' >> "$GITHUB_OUTPUT" | |
| fi | |
| fi | |
| echo 'index-repo=${{ github.event_name != 'workflow_dispatch' && 'leanprover/reservoir-index' || inputs.index-repo }}' >> "$GITHUB_OUTPUT" | |
| echo testbed-size=${{ github.event_name != 'workflow_dispatch' && 10 || toJson(inputs.testbed-size) == 'null' && -1 || inputs.testbed-size }} >> "$GITHUB_OUTPUT" | |
| echo production-deploy=${{ inputs.production-deploy || (toJson(inputs.production-deploy) == 'null' && github.ref_name == 'master') }} >> "$GITHUB_OUTPUT" | |
| testbed: | |
| needs: [config] | |
| if: needs.config.outputs.testbed == 'true' | |
| name: Testbed | |
| uses: ./.github/workflows/testbed.yml | |
| secrets: inherit | |
| with: | |
| index-repo: ${{ needs.config.outputs.index-repo }} | |
| search-packages: ${{ needs.config.outputs.search-packages == 'true' }} | |
| package-pattern: ${{ needs.config.outputs.package-pattern }} | |
| version-pattern: ${{ inputs.version-pattern }} | |
| toolchain: ${{ needs.config.outputs.testbed-toolchain }} | |
| max-size: ${{ fromJson(needs.config.outputs.testbed-size) }} | |
| cache-builds: ${{ needs.config.outputs.cache-builds == 'true' }} | |
| update-index: ${{ needs.config.outputs.update-index == 'true' }} | |
| dev: ${{ github.event_name != 'workflow_dispatch' }} | |
| website: | |
| needs: [config, testbed] | |
| # Run even if `testbed` is skipped | |
| if: (!failure() && !cancelled()) | |
| name: Website | |
| uses: ./.github/workflows/website.yml | |
| secrets: inherit | |
| with: | |
| index-repo: ${{ needs.config.outputs.index-repo }} | |
| index-artifact: ${{ needs.config.outputs.testbed == 'true' && needs.config.outputs.update-index != 'true' }} | |
| production-deploy: ${{ needs.config.outputs.production-deploy == 'true' }} |