Merge pull request #28 from Meowrium/patch-1 #50
This file contains hidden or 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 -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | |
| chmod u+x elan-init.sh | |
| ./elan-init.sh -y --default-toolchain leanprover/lean4:v4.13.0-rc3 | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| - name: Get Mathlib | |
| run: | | |
| lake exe cache get | |
| - name: Run build script | |
| run: | | |
| chmod +x scripts/mkall.py | |
| python scripts/mkall.py | |
| make html | |
| touch ./build/html/.nojekyll | |
| - 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 |