perf(to_dual): first try translating without inserting casts (#35131) #21546
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 | |
| 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 }} | |
| # 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 wan't '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 |