test.yaml

.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/<branch_name>
+      # 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 }}