DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat: Add docs in

Browse source
This commit is contained in:
jstoobysmith 2024-06-25 08:27:53 -04:00
parent 7fd3d03a65
commit 3005dc8c8c
1 changed files with 25 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

50
.github/workflows/docs.yml vendored
View file

@ -31,36 +31,36 @@ jobs:
rm 1.txt 2.txt
##################
# Remove this section if you don't want docs to be made
# - name: Install elan
# run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.0.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.0.0
# - name: Get cache
# run: ~/.elan/bin/lake -Kenv=dev exe cache get || true
- name: Get cache
run: ~/.elan/bin/lake -Kenv=dev exe cache get || true
# - name: Build project
# run: ~/.elan/bin/lake -Kenv=dev build HepLean
- name: Build project
run: ~/.elan/bin/lake -Kenv=dev build HepLean
# - 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-HepLean*
# key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
# restore-keys: |
# MathlibDoc-
- 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-HepLean*
key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
restore-keys: |
MathlibDoc-
# - name: Build documentation
# run: ~/.elan/bin/lake -Kenv=dev build HepLean:docs
- name: Build documentation
run: ~/.elan/bin/lake -Kenv=dev build HepLean:docs
# - name: Copy documentation to `docs/docs`
# run: |
# mv .lake/build/doc doc/docs
- name: Copy documentation to `docs/docs`
run: |
mv .lake/build/doc doc/docs
#End Section
##################
- name: Bundle dependencies