Skip to content

build and deploy mathlib4 docs #1585

build and deploy mathlib4 docs

build and deploy mathlib4 docs #1585

Workflow file for this run

name: build and deploy mathlib4 docs
on:
workflow_dispatch:
schedule:
- cron: '0 */8 * * *' # every 8 hours
# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
permissions:
contents: read
pages: write
id-token: write
jobs:
build:
name: build and deploy mathlib4 docs
runs-on: doc-gen
steps:
- name: clean up
run: |
rm -rf mathlib4_docs
rm -rf mathlib4
rm -rf workaround
rm -rf $HOME/.elan
rm -rf $HOME/.cache/mathlib
- name: Checkout repo
uses: actions/checkout@v4
with:
repository: leanprover-community/mathlib4_docs
path: mathlib4_docs
- name: Checkout mathlib
uses: actions/checkout@v4
with:
repository: leanprover-community/mathlib4
path: mathlib4
- name: install elan
run: |
set -o pipefail
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
echo "$HOME/.elan/bin" >> $GITHUB_PATH
- name: set default toolchain
working-directory: mathlib4
run: |
elan default $(cat lean-toolchain)
- name: get cache
working-directory: mathlib4
run: lake exe cache get
- name: build mathlib
working-directory: mathlib4
run: env LEAN_ABORT_ON_PANIC=1 lake build
- name: create dummy docs project
run: |
lake new workaround lib
cd workaround
cp -f ../mathlib4/lean-toolchain .
cp -f ../mathlib4_docs/lakefile.toml .
# doc-gen4 expects to work on github repos with at least one commit
git config user.email "[email protected]"
git config user.name "mathlib4_docs CI"
git add .
git commit -m "workaround"
git remote add origin "https://github.com/leanprover-community/workaround"
mkdir -p .lake/packages
cp -r ../mathlib4/.lake/packages/* .lake/packages
lake update
# Copy references.bib over while doc-gen lacks support for subproject references.bib
mkdir docs/
cp ../mathlib4/docs/references.bib docs/references.bib
- name: build doc-gen4
working-directory: workaround
run: |
lake build doc-gen4
- name: build import graph
working-directory: mathlib4
run: |
lake exe graph mathlib.html
- name: generate docs
working-directory: workaround
run: |
lake build Batteries:docs Qq:docs Aesop:docs ProofWidgets:docs Mathlib:docs Archive:docs Counterexamples:docs docs:docs
lake build Mathlib:docsHeader
- name: copy extra files
run: |
cp mathlib4/docs/{100.yaml,1000.yaml,overview.yaml,undergrad.yaml} workaround/.lake/build/doc
- name: copy import graph
run: |
cp mathlib4/mathlib.html workaround/.lake/build/doc
- name: Upload artifact
uses: actions/upload-pages-artifact@v3
with:
path: 'workaround/.lake/build/doc'
- name: Deploy to GitHub Pages
id: deployment
uses: actions/deploy-pages@v4
- name: clean up
if: always()
run: |
rm -rf mathlib4_docs
rm -rf mathlib4
rm -rf workaround
rm -rf $HOME/.elan
rm -rf $HOME/.cache/mathlib