Skip to content

Commit ac3581f

Browse files
authored
Merge pull request #67 from b-mehta/pitmonticone/golf-workflow
chore: refactor build workflow to use `docgen-action`
2 parents 342788a + 759bd77 commit ac3581f

1 file changed

Lines changed: 8 additions & 75 deletions

File tree

.github/workflows/build.yml

Lines changed: 8 additions & 75 deletions
Original file line numberDiff line numberDiff line change
@@ -26,82 +26,15 @@ jobs:
2626
name: Build project
2727
steps:
2828
- name: Checkout project
29-
uses: actions/checkout@v4
29+
uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
3030

31-
- name: Build Lean code
32-
uses: leanprover/lean-action@v1
33-
34-
- name: Cache Mathlib Docs
35-
uses: actions/cache@v4
36-
with:
37-
path: |
38-
docbuild/.lake/build/doc/Aesop
39-
docbuild/.lake/build/doc/Batteries
40-
docbuild/.lake/build/doc/find
41-
docbuild/.lake/build/doc/Init
42-
docbuild/.lake/build/doc/Lake
43-
docbuild/.lake/build/doc/Lean
44-
docbuild/.lake/build/doc/Mathlib
45-
docbuild/.lake/build/doc/Std
46-
key: Docs-${{ hashFiles('lake-manifest.json') }}
47-
if: github.ref == 'refs/heads/main'
48-
49-
- name: Build Documentation
50-
run: scripts/build_docs.sh
51-
if: github.ref == 'refs/heads/main'
52-
53-
- name: Build blueprint and copy to `home_page/blueprint`
54-
uses: xu-cheng/texlive-action@v2
55-
with:
56-
docker_image: ghcr.io/xu-cheng/texlive-full:20231201
57-
run: |
58-
apk update
59-
apk add --update make py3-pip git pkgconfig graphviz graphviz-dev gcc musl-dev
60-
git config --global --add safe.directory $GITHUB_WORKSPACE
61-
git config --global --add safe.directory `pwd`
62-
python3 -m venv env
63-
source env/bin/activate
64-
pip install --upgrade pip requests wheel
65-
pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/"
66-
pip install leanblueprint
67-
leanblueprint pdf
68-
cp blueprint/print/print.pdf home_page/blueprint.pdf
69-
leanblueprint web
70-
cp -r blueprint/web home_page/blueprint
71-
if: github.ref == 'refs/heads/main'
72-
73-
- name: Check declarations mentioned in the blueprint exist in Lean code
74-
run: ~/.elan/bin/lake exe checkdecls blueprint/lean_decls
75-
if: github.ref == 'refs/heads/main'
76-
77-
- name: Move documentation to `home_page/docs`
78-
run: |
79-
sudo chown -R runner home_page
80-
cp -r docbuild/.lake/build/doc home_page/docs
81-
if: github.ref == 'refs/heads/main'
82-
83-
- name: Bundle dependencies
84-
uses: ruby/setup-ruby@a4effe49ee8ee5b8b5091268c473a4628afb5651 # v1.245.0
31+
- name: Build the project
32+
uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # v1.2.0
8533
with:
86-
working-directory: home_page
87-
ruby-version: "3.1" # Specify Ruby version
88-
bundler-cache: true # Enable caching for bundler
89-
if: github.ref == 'refs/heads/main'
34+
use-github-cache: false
9035

91-
- name: Build website using Jekyll
92-
working-directory: home_page
93-
env:
94-
JEKYLL_GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
95-
if: github.ref == 'refs/heads/main'
96-
run: JEKYLL_ENV=production bundle exec jekyll build
97-
98-
- name: "Upload website (API documentation, blueprint and any home page)"
99-
uses: actions/upload-pages-artifact@56afc609e74202658d3ffba0e8f6dda462b719fa # v3.0.1
36+
- name: Compile blueprint and documentation
37+
uses: leanprover-community/docgen-action@b210116d3e6096c0c7146f7a96a6d56b6884fef5 # 2025-06-12
10038
with:
101-
path: home_page/_site/
102-
if: github.ref == 'refs/heads/main'
103-
104-
- name: Deploy to GitHub Pages
105-
id: deployment
106-
uses: actions/deploy-pages@d6db90164ac5ed86f2b6aed7e0febac5b3c0c03e # v4.0.5
107-
if: github.ref == 'refs/heads/main'
39+
blueprint: true
40+
homepage: home_page

0 commit comments

Comments
 (0)