Skip to content

Commit

Permalink
try building branch
Browse files Browse the repository at this point in the history
  • Loading branch information
fpvandoorn committed Jun 30, 2024
1 parent 04dc610 commit 6764e37
Showing 1 changed file with 99 additions and 0 deletions.
99 changes: 99 additions & 0 deletions .github/workflows/blueprint.yml
Original file line number Diff line number Diff line change
@@ -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

0 comments on commit 6764e37

Please sign in to comment.