diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index af9a92f4..c23d623a 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -1,4 +1,39 @@ - - name: Install Leanblueprint and generate web in tex env +on: + push: + branches-ignore: + - gh-pages + +jobs: + deploy: + runs-on: ubuntu-latest + steps: + - name: Checkout + uses: actions/checkout@v2 + with: + submodules: true + + - name: Setup Python + uses: actions/setup-python@v2 + with: + python-version: '3.8' + + - name: Install elan + run: | + set -o pipefail + curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -v -y + sudo ln -s $HOME/.elan/bin/* /usr/local/bin; + - name: Install python Lean dependencies + run: python -m pip install --upgrade pip requests markdown2 toml mathlibtools toposort invoke + + - name: Link and fetch mathlib + run: | + leanproject get leanprover-community/lean-liquid + ln -s lean-liquid project + cd project && leanproject get-m && scripts/fetch_olean_cache.sh && cd .. + # https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/blueprint/near/292717229 + ulimit -s 1048576 + inv decls + - name: Install Leanblueprint and generate web in tex env id: generate_files uses: xu-cheng/texlive-action/full@v1 with: @@ -19,3 +54,12 @@ mv web2 "web/$branch" fi echo "##[set-output name=keep_files;]$([[ ${GITHUB_REF##*/} == "master" ]] && echo "false" || echo "true")" + # For non-master branches we temporarily deploy to https://leanprover-community.github.io/liquid/ + # All such files will then get deleted when there's a deploy to master. + + - name: deploy + uses: peaceiris/actions-gh-pages@v3 + with: + github_token: ${{ secrets.github_token }} + publish_dir: ./web + keep_files: ${{ steps.generate_files.outputs.keep_files }}