Skip to content

Update2 push.yml

Update2 push.yml #216

Workflow file for this run

on:
push:
branches:
- master
workflow_dispatch:
# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
permissions:
contents: read
pages: write
id-token: write
jobs:
build_project:
runs-on: ubuntu-latest
name: Build project
concurrency:
group: ${{ github.workflow }}-${{ github.ref }}
cancel-in-progress: true
steps:
- name: Free Disk Space (Ubuntu)
uses: jlumbroso/free-disk-space@main
with:
# this might remove tools that are actually needed,
# if set to "true" but frees about 6 GB
tool-cache: false
# all of these default to true, but feel free to set to
# "false" if necessary for your workflow
android: true
dotnet: true
haskell: true
large-packages: true
docker-images: true
swap-storage: true
- name: Checkout project
uses: actions/checkout@v2
with:
fetch-depth: 0
- name: Install elan
run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.0.0
- name: Get cache
run: ~/.elan/bin/lake -Kenv=dev exe cache get
- name: Build project
run: ~/.elan/bin/lake -R -Kenv=dev build FltRegular
- uses: actions/cache@v3
name: Mathlib doc Cache
with:
path: build/doc/Mathlib
key: DocGen4-${{ hashFiles('lake-manifest.json') }}
restore-keys: |
DocGen4-
- name: Build documentation
run: ~/.elan/bin/lake -R -Kenv=dev build FltRegular:docs
- name: Install Python
uses: actions/setup-python@v4
with:
python-version: '3.9'
cache: 'pip' # caching pip dependencies
- name: Install blueprint apt deps
run: |
sudo apt-get update
sudo apt-get install -y graphviz libgraphviz-dev pdf2svg dvisvgm texlive-full
- name: Install blueprint deps
run: |
cd blueprint && pip install -r requirements.txt
- name: Build blueprint
run: |
cd blueprint && inv all
- name: Copy documentation
run: |
mkdir -p _site
mv .lake/build/doc _site/doc
mv blueprint/web _site/blueprint
- name: Upload doc & blueprint artifact
uses: actions/upload-pages-artifact@v1
with:
path: '_site'
- name: Deploy to GitHub Pages
id: deployment
uses: actions/deploy-pages@v1