Merge remote-tracking branch 'origin/lean-pr-testing-6535' into blizz… #3
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
| # DO NOT EDIT THIS FILE!!! | |
| # This file is automatically generated by mk_build_yml.sh | |
| # Edit .github/build.in.yml instead and run | |
| # .github/workflows/mk_build_yml.sh to update. | |
| # Forks of mathlib and other projects should be able to use build_fork.yml directly | |
| # The jobs in this file run on self-hosted workers and will not be run from external forks | |
| on: | |
| push: | |
| branches: | |
| - 'blizzard_inc/debug_ci**' | |
| name: continuous integration (windows) | |
| env: | |
| # Disable Lake's automatic fetching of cloud builds. | |
| # Lake's cache is currently incompatible with Mathlib's `lake exe cache`. | |
| # This is because Mathlib's Cache assumes all build aritfacts present in the build directory | |
| # are valid by-products of the Mathlib build. Build artifacts fetched from Lake's cache do | |
| # not necessarily satisfy this property. | |
| LAKE_NO_CACHE: true | |
| concurrency: | |
| # label each workflow run; only the latest with each label will run | |
| # workflows on master get more expressive labels | |
| group: ${{ github.workflow }}-${{ github.ref }}. | |
| ${{ ( contains(fromJSON( '["refs/heads/master", "refs/heads/staging"]'), github.ref ) && github.run_id) || ''}} | |
| # cancel any running workflow with the same label (but not on this branch) | |
| cancel-in-progress: ${{!startsWith(github.ref,'refs/heads/blizzard_inc/debug')}} | |
| jobs: | |
| windows-build: | |
| runs-on: windows-latest | |
| steps: | |
| - name: checkout | |
| uses: actions/checkout@v4 | |
| - name: install elan | |
| shell: bash | |
| run: | | |
| : Install Elan | |
| scripts/windows/install_elan.sh | |
| - name: install other compiler | |
| shell: bash | |
| run: | | |
| echo skipped | |
| - name: grab the cache | |
| shell: bash | |
| run: lake exe cache get |