1+ name : Compile blueprint
2+
3+ on :
4+ push :
5+ branches :
6+ - blueprint
7+ workflow_dispatch : # Allow manual triggering of the workflow from the GitHub Actions interface
8+
9+ # Cancel previous runs if a new commit is pushed to the same PR or branch
10+ concurrency :
11+ group : ${{ github.ref }} # Group runs by the ref (branch or PR)
12+ cancel-in-progress : true # Cancel any ongoing runs in the same group
13+
14+ # Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
15+ permissions :
16+ contents : read # Read access to repository contents
17+ pages : write # Write access to GitHub Pages
18+ id-token : write # Write access to ID tokens
19+
20+ jobs :
21+ build_project :
22+ runs-on : ubuntu-latest
23+ name : Build project
24+ steps :
25+ - name : Checkout project
26+ uses : actions/checkout@v4
27+ with :
28+ fetch-depth : 0 # Fetch all history for all branches and tags
29+
30+ - name : Install elan
31+ run : curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
32+
33+ - name : Get Mathlib cache
34+ run : ~/.elan/bin/lake exe cache get || true
35+
36+ - name : Build project
37+ run : ~/.elan/bin/lake build LeanCommAlg
38+
39+ - name : Cache mathlib API docs
40+ uses : actions/cache@v4
41+ with :
42+ path : |
43+ .lake/build/doc/Init
44+ .lake/build/doc/Lake
45+ .lake/build/doc/Lean
46+ .lake/build/doc/Std
47+ .lake/build/doc/Mathlib
48+ .lake/build/doc/declarations
49+ .lake/build/doc/find
50+ .lake/build/doc/*.*
51+ !.lake/build/doc/declarations/declaration-data-LeanCommAlg*
52+ key : MathlibDoc-${{ hashFiles('lake-manifest.json') }}
53+ restore-keys : MathlibDoc-
54+
55+ - name : Build project API documentation
56+ run : ~/.elan/bin/lake -R -Kenv=dev build LeanCommAlg:docs
57+
58+ - name : Check for `home_page` folder # this is meant to detect a Jekyll-based website
59+ id : check_home_page
60+ run : |
61+ if [ -d home_page ]; then
62+ echo "The 'home_page' folder exists in the repository."
63+ echo "HOME_PAGE_EXISTS=true" >> $GITHUB_ENV
64+ else
65+ echo "The 'home_page' folder does not exist in the repository."
66+ echo "HOME_PAGE_EXISTS=false" >> $GITHUB_ENV
67+ fi
68+
69+ name : Build blueprint and copy to `home_page/blueprint`
70+ uses : xu-cheng/texlive-action@v2
71+ with :
72+ docker_image : ghcr.io/xu-cheng/texlive-full:20231201
73+ run : |
74+ # Install necessary dependencies and build the blueprint
75+ apk update
76+ apk add --update make py3-pip git pkgconfig graphviz graphviz-dev gcc musl-dev
77+ git config --global --add safe.directory $GITHUB_WORKSPACE
78+ git config --global --add safe.directory `pwd`
79+ python3 -m venv env
80+ source env/bin/activate
81+ pip install --upgrade pip requests wheel
82+ pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/"
83+ pip install leanblueprint
84+ leanblueprint pdf
85+ mkdir -p home_page
86+ cp blueprint/print/print.pdf home_page/blueprint.pdf
87+ leanblueprint web
88+ cp -r blueprint/web home_page/blueprint
89+
90+ name : Check declarations mentioned in the blueprint exist in Lean code
91+ run : |
92+ ~/.elan/bin/lake exe checkdecls blueprint/lean_decls
93+
94+ name : Copy API documentation to `home_page/docs`
95+ run : cp -r .lake/build/doc home_page/docs
96+
97+ - name : Remove unnecessary lake files from documentation in `home_page/docs`
98+ run : |
99+ find home_page/docs -name "*.trace" -delete
100+ find home_page/docs -name "*.hash" -delete
101+
102+ name : Bundle dependencies
103+ uses : ruby/setup-ruby@v1
104+ with :
105+ working-directory : home_page
106+ ruby-version : " 3.0" # Specify Ruby version
107+ bundler-cache : true # Enable caching for bundler
108+
109+ - name : Build website using Jekyll
110+ if : env.HOME_PAGE_EXISTS == 'true'
111+ working-directory : home_page
112+ env :
113+ JEKYLL_GITHUB_TOKEN : ${{ secrets.GITHUB_TOKEN }}
114+ run : JEKYLL_ENV=production bundle exec jekyll build # Note this will also copy the blueprint and API doc into home_page/_site
115+
116+ - name : " Upload website (API documentation, blueprint and any home page)"
117+ uses : actions/upload-pages-artifact@v3
118+ with :
119+ path : ${{ env.HOME_PAGE_EXISTS == 'true' && 'home_page/_site' || 'home_page/' }}
120+
121+ - name : Deploy to GitHub Pages
122+ id : deployment
123+ uses : actions/deploy-pages@v4
124+
125+ - name : Make sure the API documentation cache works
126+ run : mv home_page/docs .lake/build/doc
127+
0 commit comments