diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml new file mode 100644 index 00000000..bd03759e --- /dev/null +++ b/.github/workflows/blueprint.yml @@ -0,0 +1,99 @@ +on: + push: + branches: + - blueprint_test + +# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages +permissions: + contents: read + pages: write + id-token: write + +jobs: + style_lint: + name: Lint style + runs-on: ubuntu-latest + steps: + - name: Check for long lines + if: always() + run: | + ! (find Carleson -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://') + +jobs: + build_project: + runs-on: ubuntu-latest + name: Build project + steps: + - name: Checkout project + uses: actions/checkout@v2 + with: + fetch-depth: 0 + + - name: Install elan + run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.5.0 + + - name: Get cache + run: ~/.elan/bin/lake exe cache get || true + + - name: Build project + run: ~/.elan/bin/lake build Carleson + + - name: Cache mathlib docs + uses: actions/cache@v3 + with: + 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 + !.lake/build/doc/declarations/declaration-data-Carleson* + key: MathlibDoc-${{ hashFiles('lake-manifest.json') }} + restore-keys: | + MathlibDoc- + + - name: Build documentation + run: ~/.elan/bin/lake -R -Kenv=dev build Carleson:docs + + - name: Build blueprint and copy to `docs/blueprint` + uses: xu-cheng/texlive-action@v2 + with: + docker_image: ghcr.io/xu-cheng/texlive-full:20231201 + run: | + apk update + 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 venv env + source env/bin/activate + pip install --upgrade pip requests wheel + pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/" + pip install leanblueprint + leanblueprint pdf + mkdir docs + cp blueprint/print/print.pdf docs/blueprint.pdf + leanblueprint web + cp -r blueprint/web docs/blueprint + + - name: Check declarations + run: | + ~/.elan/bin/lake exe checkdecls blueprint/lean_decls + + - name: Move documentation to `docs/docs` + run: | + sudo chown -R runner docs + cp -r .lake/build/doc docs/docs + + - name: Upload docs & blueprint artifact + uses: actions/upload-pages-artifact@v1 + with: + path: docs/ + + - 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 \ No newline at end of file