Skip to content

build: Remove doc regeneration on doc/main #16

build: Remove doc regeneration on doc/main

build: Remove doc regeneration on doc/main #16

Workflow file for this run

name: deploy-docs
on:
push:
branches:
- 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
with:
submodules: true
- name: Install Python
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: Install Lean
run: |
elan toolchain install $(<src/lean-toolchain)
- 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