.github/workflows/main.yml #12

	on: workflow_dispatch


	# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
	permissions:
	contents: write

	jobs:
	build_project:
	runs-on: ubuntu-latest
	name: Build project
	concurrency:
	group: ${{ github.workflow }}-${{ github.ref }}
	cancel-in-progress: true
	steps:
	- 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 -Kenv=dev build FltRegular

	- name: Build documentation
	run: ~/.elan/bin/lake -Kenv=dev build Std:docs Mathlib:docs 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 build/doc _site/doc
	mv blueprint/web _site/blueprint

	- name: Deploy doc & blueprint
	uses: peaceiris/actions-gh-pages@v3
	with:
	github_token: ${{ secrets.github_token }}
	publish_dir: _site

Provide feedback