Skip to content

chore: Fix build task names and check lake #6

chore: Fix build task names and check lake

chore: Fix build task names and check lake #6

Workflow file for this run

name: deploy-docs
# Run this when the master or main branch changes
on:
push:
branches:
- main
- doc/main
# This job installs dependencies, builds the book, and pushes it to `gh-pages`
jobs:
deploy-book:
runs-on: ubuntu-latest
permissions:
pages: write
id-token: write
steps:
- uses: actions/checkout@v3
# Install dependencies
- name: Set up Python 3.11
uses: actions/setup-python@v4
with:
python-version: 3.11
- name: Install elan
run: |
set -o pipefail
curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
./elan-init -y --default-toolchain none
echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
- name: Print lean and lake versions
run: |
lake --version
- name: Install poetry
run: |
pip install poetry
poetry install --only doc
- name: Build documentations
run: |
poetry run jupyter-book build docs
# Upload the book's HTML as an artifact
- name: Upload artifact
uses: actions/upload-pages-artifact@v2
with:
path: "docs/_build/html"
# Deploy the book's HTML to GitHub Pages
- name: Deploy to GitHub Pages
id: deployment
uses: actions/deploy-pages@v2