fix: Update _config with repo
This commit is contained in:
parent
be1981cc56
commit
7fd3d03a65
2 changed files with 33 additions and 31 deletions
62
.github/workflows/docs.yml
vendored
62
.github/workflows/docs.yml
vendored
|
@ -29,38 +29,40 @@ jobs:
|
|||
mkdir -p docs/_includes
|
||||
comm -23 1.txt 2.txt | sed -e 's/^\(.*\)$/- [`\1`](https:\/\/github.com\/teorth\/HepLean\/blob\/master\/\1)/' > docs/_includes/files_to_upstream.md
|
||||
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: Get cache
|
||||
# run: ~/.elan/bin/lake -Kenv=dev exe cache get || true
|
||||
|
||||
# - 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: 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: 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: 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: Build documentation
|
||||
# run: ~/.elan/bin/lake -Kenv=dev build HepLean:docs
|
||||
|
||||
# - name: Copy documentation to `docs/docs`
|
||||
# run: |
|
||||
# mv .lake/build/doc doc/docs
|
||||
#End Section
|
||||
##################
|
||||
- name: Bundle dependencies
|
||||
uses: ruby/setup-ruby@v1
|
||||
with:
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue