feat(Combinatorics/SimpleGraph/Maps): every homomorphism f : H →g G…
#22755
This file contains hidden or 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: continuous integration (staging) | |
| on: | |
| push: | |
| branches: | |
| - staging | |
| - trying | |
| concurrency: | |
| # label each workflow run; only the latest with each label will run | |
| group: ${{ github.workflow }}-${{ github.ref }}-${{ 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 (staging) | |
| 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.run_id }} | |
| pr_branch_ref: ${{ github.sha }} | |
| # Use the MASTER cache key only when merging into mathlib4 (staging branch); | |
| # 'bors try' runs (trying branch) and nightly-testing use NON_MASTER | |
| cache_application_id: ${{ github.ref_name == 'staging' && github.repository == 'leanprover-community/mathlib4' && vars.CACHE_MASTER_WRITER_AZURE_APP_ID || vars.CACHE_NON_MASTER_WRITER_AZURE_APP_ID }} | |
| # bors runs should build the tools from their commit-under-test: after all, we are trying to | |
| # test 'what would happen if this was merged', so we need to use the 'would-be-post-merge' tools | |
| tools_branch_ref: ${{ github.sha }} | |
| # We don't want 'bors try' runs to compete with merge-candidates, so we pool trying with PR runs | |
| runs_on: ${{ github.ref_name == 'trying' && 'pr' || 'bors' }} | |
| secrets: inherit |