From b0b257fbe2b7ccdc81e78bee9c4ab17f5b49fb6a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Tue, 12 Dec 2023 19:55:33 +0100 Subject: [PATCH] Fancy new workflow with doc caching that works --- .github/workflows/push.yml | 90 +++++++++++++++++------------------ .github/workflows/push_pr.yml | 19 +++++++- 2 files changed, 62 insertions(+), 47 deletions(-) diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index 4e5facc8ca..fa6a713490 100644 --- a/.github/workflows/push.yml +++ b/.github/workflows/push.yml @@ -10,29 +10,24 @@ permissions: id-token: write jobs: + style_lint: + name: Lint style + runs-on: ubuntu-latest + steps: + - name: Check for long lines + if: always() + run: | + ! (find LeanAPAP -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://') + + - name: Don't 'import Mathlib', use precise imports + if: always() + run: | + ! (find LeanAPAP -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Mathlib$') + build_project: runs-on: ubuntu-latest name: Build project - concurrency: - group: ${{ github.workflow }}-${{ github.ref }} - cancel-in-progress: true steps: - # - name: Free disk space - # uses: jlumbroso/free-disk-space@main - # with: - # # this might remove tools that are actually needed, - # # if set to "true" but frees about 6 GB - # tool-cache: false - - # # all of these default to true, but feel free to set to - # # "false" if necessary for your workflow - # android: true - # dotnet: true - # haskell: true - # large-packages: true - # docker-images: true - # swap-storage: true - - name: Checkout project uses: actions/checkout@v2 with: @@ -42,18 +37,14 @@ jobs: run: | grep -r --files-without-match 'import LeanAPAP' LeanAPAP | sort > 1.txt grep -r --files-with-match 'sorry' LeanAPAP | sort > 2.txt - mkdir -p docs/_includes - comm -23 1.txt 2.txt | sed -e 's/^\(.*\)$/- [`\1`](https:\/\/github.com\/YaelDillies\/LeanAPAP\/blob\/main\/\1)/' > docs/_includes/files_to_upstream.md + comm -23 1.txt 2.txt | sed -e 's/^\(.*\)$/- [`\1`](https:\/\/github.com\/YaelDillies\/LeanAPAP\/blob\/master\/\1)/' > docs/_includes/files_to_upstream.md rm 1.txt 2.txt - - name: Count sorries - run: python scripts/count_sorry.py - - name: Install elan run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.0.0 - name: Get cache - run: ~/.elan/bin/lake -Kenv=dev exe cache get + run: ~/.elan/bin/lake -Kenv=dev exe cache get || true - name: Build project run: ~/.elan/bin/lake -Kenv=dev build LeanAPAP @@ -61,36 +52,39 @@ jobs: - name: Cache mathlib docs uses: actions/cache@v3 with: - path: build/doc/Mathlib - key: DocGen4-${{ hashFiles('lake-manifest.json') }} + path: | + .lake/build/doc/Init + .lake/build/doc/Lake + .lake/build/doc/Lean + .lake/build/doc/Std + .lake/build/doc/Mathlib + .lake/build/doc/declarations + key: MathlibDoc-${{ hashFiles('lake-manifest.json') }} restore-keys: | - DocGen4- + MathlibDoc- - name: Build documentation run: ~/.elan/bin/lake -Kenv=dev build LeanAPAP:docs - - name: Install Python - uses: actions/setup-python@v4 - with: - python-version: '3.9' - cache: 'pip' # caching pip dependencies - - - name: Install blueprint apt dependencies - run: | - sudo apt-get update - sudo apt-get install -y graphviz libgraphviz-dev pdf2svg dvisvgm texlive-full - - - name: Install blueprint dependencies - run: | - cd blueprint && pip install -r requirements.txt - - name: Build blueprint and copy to `docs/blueprint` - run: | - inv all + uses: xu-cheng/texlive-action@v2 + with: + scheme: full + run: | + apk update + apk add --update make py3-pip git + apk add --update make py3-pip git pkgconfig graphviz graphviz-dev gcc musl-dev + git config --global --add safe.directory $GITHUB_WORKSPACE + git config --global --add safe.directory `pwd` + python3 -m pip install --upgrade pip requests wheel + python3 -m pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/" + pip install -r blueprint/requirements.txt + python3 -m pip install invoke + inv all - name: Copy documentation to `docs/docs` run: | - mv build/doc docs/docs + mv .lake/build/doc docs/docs - name: Bundle dependencies uses: ruby/setup-ruby@v1 @@ -111,3 +105,7 @@ jobs: - name: Deploy to GitHub Pages id: deployment uses: actions/deploy-pages@v1 + + - name: Make sure the cache works + run: | + mv docs/docs .lake/build/doc diff --git a/.github/workflows/push_pr.yml b/.github/workflows/push_pr.yml index ae0ae924dc..9b2e8f4953 100644 --- a/.github/workflows/push_pr.yml +++ b/.github/workflows/push_pr.yml @@ -1,7 +1,24 @@ on: pull_request: + push: + branches-ignore: + - master jobs: + style_lint: + name: Lint style + runs-on: ubuntu-latest + steps: + - name: Check for long lines + if: always() + run: | + ! (find LeanAPAP -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://') + + - name: Don't 'import Mathlib', use precise imports + if: always() + run: | + ! (find LeanAPAP -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Mathlib$') + build_project: runs-on: ubuntu-latest name: Build project @@ -18,7 +35,7 @@ jobs: run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.0.0 - name: Get cache - run: ~/.elan/bin/lake exe cache get + run: ~/.elan/bin/lake exe cache get || true - name: Build project run: ~/.elan/bin/lake build LeanAPAP