Skip to content

Commit 0d97f86

Browse files
justin-t-morrilljustin-t-morrill
committed
Rebased
2 parents e2fa43f + d78b6af commit 0d97f86

36 files changed

Lines changed: 3397 additions & 146 deletions

‎.github/workflows/blueprint 2.yml‎

Lines changed: 125 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,125 @@
1+
name: Compile blueprint
2+
3+
on:
4+
push:
5+
branches:
6+
- main # Trigger on pushes to the default branch
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 Game
38+
39+
- name: Cache API docs
40+
uses: actions/cache@v4
41+
with:
42+
path: |
43+
.lake/build/doc/Aesop
44+
.lake/build/doc/Batteries
45+
.lake/build/doc/find
46+
.lake/build/doc/Init
47+
.lake/build/doc/Lake
48+
.lake/build/doc/Lean
49+
.lake/build/doc/Mathlib
50+
.lake/build/doc/Std
51+
key: Docs-${{ hashFiles('lake-manifest.json') }}
52+
53+
- name: Build project API documentation
54+
run: ~/.elan/bin/lake -R -Kenv=dev build Game:docs
55+
56+
- name: Check for `home_page` folder # this is meant to detect a Jekyll-based website
57+
id: check_home_page
58+
run: |
59+
if [ -d home_page ]; then
60+
echo "The 'home_page' folder exists in the repository."
61+
echo "HOME_PAGE_EXISTS=true" >> $GITHUB_ENV
62+
else
63+
echo "The 'home_page' folder does not exist in the repository."
64+
echo "HOME_PAGE_EXISTS=false" >> $GITHUB_ENV
65+
fi
66+
67+
- name: Build blueprint and copy to `home_page/blueprint`
68+
uses: xu-cheng/texlive-action@v2
69+
with:
70+
docker_image: ghcr.io/xu-cheng/texlive-full:20250101
71+
run: |
72+
# Install necessary dependencies and build the blueprint
73+
apk update
74+
apk add --update make py3-pip git pkgconfig graphviz graphviz-dev gcc musl-dev
75+
git config --global --add safe.directory $GITHUB_WORKSPACE
76+
git config --global --add safe.directory `pwd`
77+
python3 -m venv env
78+
source env/bin/activate
79+
pip install --upgrade pip requests wheel
80+
pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/"
81+
pip install leanblueprint
82+
leanblueprint pdf
83+
mkdir -p home_page
84+
cp blueprint/print/print.pdf home_page/blueprint.pdf
85+
leanblueprint web
86+
cp -r blueprint/web home_page/blueprint
87+
88+
- name: Check declarations mentioned in the blueprint exist in Lean code
89+
run: |
90+
~/.elan/bin/lake exe checkdecls blueprint/lean_decls
91+
92+
- name: Copy API documentation to `home_page/docs`
93+
run: cp -r .lake/build/doc home_page/docs
94+
95+
- name: Remove unnecessary lake files from documentation in `home_page/docs`
96+
run: |
97+
find home_page/docs -name "*.trace" -delete
98+
find home_page/docs -name "*.hash" -delete
99+
100+
- name: Bundle dependencies
101+
uses: ruby/setup-ruby@v1
102+
with:
103+
working-directory: home_page
104+
ruby-version: "3.0" # Specify Ruby version
105+
bundler-cache: true # Enable caching for bundler
106+
107+
- name: Build website using Jekyll
108+
if: env.HOME_PAGE_EXISTS == 'true'
109+
working-directory: home_page
110+
env:
111+
JEKYLL_GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
112+
run: JEKYLL_ENV=production bundle exec jekyll build # Note this will also copy the blueprint and API doc into home_page/_site
113+
114+
- name: "Upload website (API documentation, blueprint and any home page)"
115+
uses: actions/upload-pages-artifact@v3
116+
with:
117+
path: ${{ env.HOME_PAGE_EXISTS == 'true' && 'home_page/_site' || 'home_page/' }}
118+
119+
- name: Deploy to GitHub Pages
120+
id: deployment
121+
uses: actions/deploy-pages@v4
122+
123+
- name: Make sure the API documentation cache works
124+
run: mv home_page/docs .lake/build/doc
125+

‎.github/workflows/blueprint 3.yml‎

Lines changed: 125 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,125 @@
1+
name: Compile blueprint
2+
3+
on:
4+
push:
5+
branches:
6+
- main # Trigger on pushes to the default branch
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 Game
38+
39+
- name: Cache API docs
40+
uses: actions/cache@v4
41+
with:
42+
path: |
43+
.lake/build/doc/Aesop
44+
.lake/build/doc/Batteries
45+
.lake/build/doc/find
46+
.lake/build/doc/Init
47+
.lake/build/doc/Lake
48+
.lake/build/doc/Lean
49+
.lake/build/doc/Mathlib
50+
.lake/build/doc/Std
51+
key: Docs-${{ hashFiles('lake-manifest.json') }}
52+
53+
- name: Build project API documentation
54+
run: ~/.elan/bin/lake -R -Kenv=dev build Game:docs
55+
56+
- name: Check for `home_page` folder # this is meant to detect a Jekyll-based website
57+
id: check_home_page
58+
run: |
59+
if [ -d home_page ]; then
60+
echo "The 'home_page' folder exists in the repository."
61+
echo "HOME_PAGE_EXISTS=true" >> $GITHUB_ENV
62+
else
63+
echo "The 'home_page' folder does not exist in the repository."
64+
echo "HOME_PAGE_EXISTS=false" >> $GITHUB_ENV
65+
fi
66+
67+
- name: Build blueprint and copy to `home_page/blueprint`
68+
uses: xu-cheng/texlive-action@v2
69+
with:
70+
docker_image: ghcr.io/xu-cheng/texlive-full:20250101
71+
run: |
72+
# Install necessary dependencies and build the blueprint
73+
apk update
74+
apk add --update make py3-pip git pkgconfig graphviz graphviz-dev gcc musl-dev
75+
git config --global --add safe.directory $GITHUB_WORKSPACE
76+
git config --global --add safe.directory `pwd`
77+
python3 -m venv env
78+
source env/bin/activate
79+
pip install --upgrade pip requests wheel
80+
pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/"
81+
pip install leanblueprint
82+
leanblueprint pdf
83+
mkdir -p home_page
84+
cp blueprint/print/print.pdf home_page/blueprint.pdf
85+
leanblueprint web
86+
cp -r blueprint/web home_page/blueprint
87+
88+
- name: Check declarations mentioned in the blueprint exist in Lean code
89+
run: |
90+
~/.elan/bin/lake exe checkdecls blueprint/lean_decls
91+
92+
- name: Copy API documentation to `home_page/docs`
93+
run: cp -r .lake/build/doc home_page/docs
94+
95+
- name: Remove unnecessary lake files from documentation in `home_page/docs`
96+
run: |
97+
find home_page/docs -name "*.trace" -delete
98+
find home_page/docs -name "*.hash" -delete
99+
100+
- name: Bundle dependencies
101+
uses: ruby/setup-ruby@v1
102+
with:
103+
working-directory: home_page
104+
ruby-version: "3.0" # Specify Ruby version
105+
bundler-cache: true # Enable caching for bundler
106+
107+
- name: Build website using Jekyll
108+
if: env.HOME_PAGE_EXISTS == 'true'
109+
working-directory: home_page
110+
env:
111+
JEKYLL_GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
112+
run: JEKYLL_ENV=production bundle exec jekyll build # Note this will also copy the blueprint and API doc into home_page/_site
113+
114+
- name: "Upload website (API documentation, blueprint and any home page)"
115+
uses: actions/upload-pages-artifact@v3
116+
with:
117+
path: ${{ env.HOME_PAGE_EXISTS == 'true' && 'home_page/_site' || 'home_page/' }}
118+
119+
- name: Deploy to GitHub Pages
120+
id: deployment
121+
uses: actions/deploy-pages@v4
122+
123+
- name: Make sure the API documentation cache works
124+
run: mv home_page/docs .lake/build/doc
125+

0 commit comments

Comments
 (0)