Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[doc-gen] Use docbuild setup #60

Draft
wants to merge 5 commits into
base: master
Choose a base branch
from
Draft

[doc-gen] Use docbuild setup #60

Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
c41e038
Update blueprint.yml
pitmonticone Oct 8, 2024
29b294c
Revert "Update blueprint.yml"
pitmonticone Oct 8, 2024
d524632
Merge remote-tracking branch 'upstream/master'
pitmonticone Oct 9, 2024
20bff8a
use new doc-gen setup
pitmonticone Nov 11, 2024
9b09ecc
fix
pitmonticone Nov 11, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
25 changes: 13 additions & 12 deletions leanblueprint/templates/blueprint.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,20 +40,21 @@ jobs:
uses: actions/cache@v4
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/find
.lake/build/doc/*.*
!.lake/build/doc/declarations/declaration-data-{| lib_name |}*
./docbuild/.lake/build/doc/Init
./docbuild/.lake/build/doc/Lake
./docbuild/.lake/build/doc/Lean
./docbuild/.lake/build/doc/Std
./docbuild/.lake/build/doc/Mathlib
./docbuild/.lake/build/doc/declarations
./docbuild/.lake/build/doc/find
./docbuild/.lake/build/doc/*.*
!./docbuild/.lake/build/doc/declarations/declaration-data-{| lib_name |}*
key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
restore-keys: MathlibDoc-

- name: Build project API documentation
run: ~/.elan/bin/lake -R -Kenv=dev build {| lib_name |}:docs
working-directory: ./docbuild
run: ~/.elan/bin/lake build {| lib_name |}:docs

- name: Check for `home_page` folder # this is meant to detect a Jekyll-based website
id: check_home_page
Expand Down Expand Up @@ -92,7 +93,7 @@ jobs:
~/.elan/bin/lake exe checkdecls blueprint/lean_decls

- name: Copy API documentation to `home_page/docs`
run: cp -r .lake/build/doc home_page/docs
run: cp -r ./docbuild/.lake/build/doc home_page/docs

- name: Remove unnecessary lake files from documentation in `home_page/docs`
run: |
Expand Down Expand Up @@ -121,5 +122,5 @@ jobs:
uses: actions/deploy-pages@v4

- name: Make sure the API documentation cache works
run: mv home_page/docs .lake/build/doc
run: mv home_page/docs ./docbuild/.lake/build/doc