build and deploy site and lib*.zip #799
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: build and deploy site and lib*.zip | |
| on: | |
| schedule: | |
| - cron: '0 3 * * *' # every day | |
| push: | |
| branches-ignore: | |
| - 'gh-pages' | |
| pull_request: | |
| branches-ignore: | |
| - 'gh-pages' | |
| # Allows you to run this workflow manually from the Actions tab | |
| workflow_dispatch: | |
| jobs: | |
| build: | |
| name: build and deploy site | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout repo | |
| uses: actions/checkout@v2 | |
| - name: install elan | |
| run: | | |
| set -o pipefail | |
| curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| - name: Get Lean version | |
| run: | | |
| set -o pipefail | |
| source elan_setup.sh | |
| echo "LATEST_BROWSER_LEAN=$LATEST_BROWSER_LEAN" >> $GITHUB_ENV | |
| - name: install Python | |
| uses: actions/setup-python@v1 | |
| with: | |
| python-version: 3.8 | |
| - name: install leanproject | |
| run: | | |
| python -m pip install --upgrade pip mathlibtools | |
| - name: generate libcore.zip | |
| run: | | |
| elan override set leanprover-community/lean:$LATEST_BROWSER_LEAN | |
| ./mk_library.py -c -o dist/libcore.zip | python detect_errors.py | |
| - name: upload libcore.zip artifact | |
| uses: actions/upload-artifact@v2 | |
| with: | |
| name: libcore | |
| path: ./dist/libcore.zip | |
| - name: upload libcore_meta.zip artifact | |
| uses: actions/upload-artifact@v2 | |
| with: | |
| name: libcore_meta | |
| path: ./dist/libcore.*.json | |
| - name: generate library.zip | |
| run: | | |
| rm -rf .git/ | |
| cd combined_lib/ | |
| git init | |
| elan override set leanprover-community/lean:$LATEST_BROWSER_LEAN | |
| leanproject --no-lean-upgrade up | |
| leanproject get-mathlib-cache | |
| rm -rf _target/deps/mathlib/test | |
| rm -rf _target/deps/mathlib/scripts | |
| rm -rf _target/deps/mathlib/roadmap | |
| cd .. | |
| ./mk_library.py -i combined_lib | python detect_errors.py | |
| - name: upload library.zip artifact | |
| uses: actions/upload-artifact@v2 | |
| with: | |
| name: library | |
| path: ./dist/library.zip | |
| - name: upload library_meta.zip artifact | |
| uses: actions/upload-artifact@v2 | |
| with: | |
| name: library_meta | |
| path: ./dist/library.*.json | |
| - name: Checkout lean-fibonacci | |
| run: git clone https://github.com/bryangingechen/lean-fibonacci.git | |
| - name: generate libfib.zip | |
| run: | | |
| cd lean-fibonacci/ | |
| elan override set leanprover-community/lean:$LATEST_BROWSER_LEAN | |
| leanpkg upgrade # don't get oleans, build for minimized libfib.zip | |
| cd .. | |
| ./mk_library.py -i lean-fibonacci -o dist/libfib.zip | python detect_errors.py | |
| - name: upload libfib.zip artifact | |
| uses: actions/upload-artifact@v2 | |
| with: | |
| name: libfib | |
| path: ./dist/libfib.zip | |
| - name: upload libfib_meta.zip artifact | |
| uses: actions/upload-artifact@v2 | |
| with: | |
| name: libfib_meta | |
| path: ./dist/libfib.*.json | |
| - name: build site and deploy | |
| run: | | |
| ./deploy.sh | |
| - name: Upload artifact | |
| uses: actions/upload-pages-artifact@v1 | |
| with: | |
| path: 'dist' | |
| # Deploy job | |
| deploy: | |
| # Add a dependency to the build job | |
| needs: build | |
| # Grant GITHUB_TOKEN the permissions required to make a Pages deployment | |
| permissions: | |
| pages: write # to deploy to Pages | |
| id-token: write # to verify the deployment originates from an appropriate source | |
| # Deploy to the github-pages environment | |
| environment: | |
| name: github-pages | |
| url: ${{ steps.deployment.outputs.page_url }} | |
| # Specify runner + deployment step | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Deploy to GitHub Pages | |
| id: deployment | |
| uses: actions/deploy-pages@v1 |