mathport #3674
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
| on: | |
| push: | |
| branches-ignore: | |
| # master is done by cron | |
| - 'master' | |
| # ignore tmp branches used by bors | |
| - 'staging.tmp*' | |
| - 'trying.tmp*' | |
| - 'staging*.tmp' | |
| schedule: | |
| - cron: '30 5 * * *' # 6:30 AM CET/9:30 PM PT | |
| workflow_dispatch: | |
| name: mathport | |
| jobs: | |
| # Cancels previous runs of jobs in this file | |
| cancel: | |
| if: github.repository == 'leanprover-community/mathport' | |
| name: 'Cancel Previous Runs (CI)' | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: styfle/[email protected] | |
| with: | |
| all_but_latest: true | |
| access_token: ${{ github.token }} | |
| build: | |
| name: Mathport | |
| runs-on: mathport | |
| steps: | |
| - name: clean up | |
| run: | | |
| rm -rf * | |
| rm -rf $HOME/.elan | |
| rm -rf $HOME/.cache/mathlib | |
| - name: install elan | |
| run: | | |
| set -o pipefail | |
| curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz | |
| ./elan-init -y --default-toolchain none | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| - uses: actions/checkout@v4 | |
| - name: get cache | |
| run: lake exe cache get | |
| - name: build mathport | |
| run: lake build | |
| - name: install jq | |
| run: | | |
| curl -sSfL https://github.com/stedolan/jq/releases/download/jq-1.6/jq-linux64 >~/.elan/bin/jq | |
| chmod +x ~/.elan/bin/jq | |
| - name: download predata | |
| run: | | |
| TAG=$(./latest-predata-release.sh) | |
| ./download-predata.sh $TAG | |
| mkdir -p Outputs/oleans/leanbin Outputs/oleans/mathbin | |
| echo $TAG > Outputs/oleans/leanbin/predata-tag | |
| echo $TAG > Outputs/oleans/mathbin/predata-tag | |
| cp sources/lean/library/upstream-rev Outputs/oleans/leanbin/ | |
| cp sources/mathlib/upstream-rev Outputs/oleans/mathbin/ | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| - name: run mathport on Lean 3 | |
| run: env time -v make port-lean | |
| - name: run mathport on mathlib | |
| run: env time -v make port-mathbin | |
| - name: prepare tarballs for release | |
| run: make mathport-tarballs | |
| - name: set tag (non-master) | |
| if: github.ref != 'refs/heads/master' | |
| run: echo "TAG=pr-${GITHUB_REF##*/}" >> $GITHUB_ENV && echo "SHORT_SHA=`git rev-parse --short HEAD`" >> $GITHUB_ENV | |
| - name: set tag (master) | |
| if: github.ref == 'refs/heads/master' | |
| run: echo "TAG=nightly-$(date -u +%F-%H)" >> $GITHUB_ENV | |
| - name: release (non-master) | |
| if: github.ref != 'refs/heads/master' | |
| uses: softprops/action-gh-release@v1 | |
| with: | |
| prerelease: true | |
| tag_name: ${{ env.TAG }}-${{ env.SHORT_SHA }} | |
| target_commitish: ${{ github.sha }} | |
| files: | | |
| lean3-binport.tar.gz | |
| lean3-synport.tar.gz | |
| mathlib3-binport.tar.gz | |
| mathlib3-synport.tar.gz | |
| archive-synport.tar.gz | |
| counterexamples-synport.tar.gz | |
| - name: release (master) | |
| if: github.ref == 'refs/heads/master' | |
| uses: softprops/action-gh-release@v1 | |
| with: | |
| prerelease: true | |
| tag_name: ${{ env.TAG }} | |
| target_commitish: ${{ github.sha }} | |
| files: | | |
| lean3-binport.tar.gz | |
| lean3-synport.tar.gz | |
| mathlib3-binport.tar.gz | |
| mathlib3-synport.tar.gz | |
| archive-synport.tar.gz | |
| counterexamples-synport.tar.gz | |
| - name: update port repos (master) | |
| if: github.ref == 'refs/heads/master' | |
| run: ./update_ports.sh | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.PUSH_NIGHTLY_TOKEN }} | |
| - name: clean up | |
| if: always() | |
| run: | | |
| rm -rf * | |
| rm -rf $HOME/.elan | |
| rm -rf $HOME/.cache/mathlib |