Delete .github/workflows/build.yml #2
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
name: Build and Deploy to GitHub Pages | |
on: | |
push: | |
branches: | |
- master # 根据您的默认分支名称进行修改 | |
jobs: | |
build-and-deploy: | |
runs-on: ubuntu-latest | |
steps: | |
- name: Checkout | |
uses: actions/checkout@v3 | |
- name: Setup Python | |
uses: actions/setup-python@v4 | |
with: | |
python-version: '3.9' | |
- name: Install dependencies | |
run: | | |
python -m pip install --upgrade pip | |
pip install -r scripts/requirements.txt | |
- name: Install Lean toolchain | |
run: | | |
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh | |
echo 'export PATH="$HOME/.elan/bin:$PATH"' >> $GITHUB_ENV | |
source $GITHUB_ENV | |
elan default leanprover/lean4:stable | |
- name: Get Mathlib | |
run: | | |
lake exe cache get | |
- name: Run build script | |
run: | | |
chmod +x scripts/mkall.py | |
python scripts/mkall.py | |
make html | |
- name: Deploy 🚀 | |
uses: JamesIves/[email protected] | |
with: | |
branch: gh-pages | |
folder: ./build/html | |
# - name: Deploy to GitHub Pages | |
# uses: peaceiris/actions-gh-pages@v3 | |
# with: | |
# github_token: ${{ secrets.GITHUB_TOKEN }} | |
# publish_dir: ./build/html | |
# destination_branch: gh-pages |