Skip to content

Commit

Permalink
update CI workflow
Browse files Browse the repository at this point in the history
  • Loading branch information
Seasawher committed Dec 25, 2024
1 parent 693ebfe commit 63038ef
Show file tree
Hide file tree
Showing 3 changed files with 9 additions and 19 deletions.
5 changes: 3 additions & 2 deletions .github/workflows/book.yml
Original file line number Diff line number Diff line change
Expand Up @@ -11,11 +11,12 @@ jobs:
book:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v3
- name: checkout
uses: actions/checkout@v4

- name: install elan
run: |
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain $(cat lean-toolchain)
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
echo "$HOME/.elan/bin" >> $GITHUB_PATH
- name: build markdown files by mdgen
Expand Down
17 changes: 3 additions & 14 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -14,18 +14,7 @@ jobs:
- name: checkout
uses: actions/checkout@v4

- name: install elan
run: |
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain $(cat lean-toolchain)
echo "$HOME/.elan/bin" >> $GITHUB_PATH
- name: Cache dependencies
uses: actions/cache@v3
- name: lean action
uses: leanprover/lean-action@v1
with:
path: .lake
key: deps-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
restore-keys: |
deps-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}
- name: lake build
run: lake build --quiet
build-args: "--log-level=warning"
6 changes: 3 additions & 3 deletions .github/workflows/deploy.yml
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ jobs:

- name: install elan
run: |
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain $(cat lean-toolchain)
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
echo "$HOME/.elan/bin" >> $GITHUB_PATH
- name: build markdown files by mdgen
Expand All @@ -43,7 +43,7 @@ jobs:
run: mdbook build

- name: upload artifact
uses: actions/upload-pages-artifact@v2
uses: actions/upload-pages-artifact@v3
with:
path: ./book

Expand All @@ -57,4 +57,4 @@ jobs:
steps:
- name: Deploy to GitHub Pages
id: deployment
uses: actions/deploy-pages@v3
uses: actions/deploy-pages@v4

0 comments on commit 63038ef

Please sign in to comment.