Skip to content

fix: typo

fix: typo #1695

Workflow file for this run

name: Compile blueprint
on:
push:
branches:
- main
paths:
- '**/*.lean'
- '**/blueprint.yml'
- 'blueprint/**'
- 'commentary/**'
- 'home_page/**'
- '**/generate_dashboard.py'
- '**/generate_equation_implication_js.py'
- '**/generate_graphiti_data.rb'
- 'lean-toolchain'
- 'lakefile.toml'
- 'lake-manifest.json'
pull_request:
branches:
- main
paths:
- '**/*.lean'
- '**/blueprint.yml'
- 'blueprint/**'
- 'commentary/**'
- 'home_page/**'
- '**/generate_dashboard.py'
- '**/generate_equation_implication_js.py'
- '**/generate_graphiti_data.rb'
- 'lean-toolchain'
- 'lakefile.toml'
- 'lake-manifest.json'
workflow_dispatch: # Allow manual triggering of the workflow from the GitHub Actions interface
# Cancel previous runs if a new commit is pushed to the same PR or branch
concurrency:
group: ${{ github.ref }} # Group runs by the ref (branch or PR)
cancel-in-progress: true # Cancel any ongoing runs in the same group
# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages and modify PR labels
permissions:
contents: read # Read access to repository contents
pages: write # Write access to GitHub Pages
id-token: write # Write access to ID tokens
issues: write # Write access to issues
pull-requests: write # Write access to pull requests
jobs:
build_project:
runs-on: ubuntu-latest
name: Build project
steps:
- name: Add 'awaiting-CI' label
if: >
github.event_name == 'pull_request'
run: |
curl --request POST \
--url https://github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels \
--header 'authorization: Bearer ${{ secrets.PAT_TOKEN }}' \
--header 'Content-Type: application/json' \
--data '["awaiting-CI"]'
- name: Checkout project
uses: actions/checkout@v4
with:
fetch-depth: 0 # Fetch all history for all branches and tags
- name: Install elan
run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
- name: Get Mathlib cache
run: ~/.elan/bin/lake exe cache get || true
- name: Cache build artifacts and Mathlib API docs
uses: actions/cache@v4
with:
path: |
.lake/build
!.lake/build/doc-data
!.lake/build/doc/declarations/declaration-data-equational_theories*
key: LakeBuild-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
restore-keys: LakeBuild-
- name: Build project
run: ~/.elan/bin/lake build equational_theories
- name: check environment with lean4checker
run: |
: Check Environment with lean4checker
chmod +x ./scripts/lean4_checker/run_lean4checker.sh
./scripts/lean4_checker/run_lean4checker.sh
shell: bash
- name: Build project API documentation
run: ~/.elan/bin/lake -R -Kenv=dev build equational_theories:docs
- name: Check for `home_page` folder
id: check_home_page
run: |
if [ -d home_page ]; then
echo "The 'home_page' folder exists in the repository."
echo "HOME_PAGE_EXISTS=true" >> $GITHUB_ENV
else
echo "The 'home_page' folder does not exist in the repository."
echo "HOME_PAGE_EXISTS=false" >> $GITHUB_ENV
fi
- name: Build blueprint and copy to `home_page/blueprint`
uses: xu-cheng/texlive-action@v2
with:
docker_image: ghcr.io/xu-cheng/texlive-full:20231201
run: |
# Install necessary dependencies and build the blueprint
apk update
apk add --update make py3-pip git pkgconfig graphviz graphviz-dev gcc musl-dev
git config --global --add safe.directory $GITHUB_WORKSPACE
git config --global --add safe.directory `pwd`
python3 -m venv env
source env/bin/activate
pip install --upgrade pip requests wheel
pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/"
pip install leanblueprint
leanblueprint pdf
mkdir -p home_page
cp blueprint/print/print.pdf home_page/blueprint.pdf
leanblueprint web
cp -r blueprint/web home_page/blueprint
- name: Check declarations mentioned in the blueprint exist in Lean code
run: |
~/.elan/bin/lake exe checkdecls blueprint/lean_decls
- name: Check with lean4lean
run: |
python scripts/lean4lean_checker/main.py
- name: Copy API documentation to `home_page/docs`
run: cp -r .lake/build/doc home_page/docs
- name: Remove unnecessary lake files from documentation in `home_page/docs`
run: |
find home_page/docs -name "*.trace" -delete
find home_page/docs -name "*.hash" -delete
- name: Generate home_page/dashboard.md
run: |
pip install pillow
python scripts/generate_dashboard.py
- name: Generate home_page/implications/implications.js
run: |
~/.elan/bin/lake exe extract_implications outcomes > /tmp/out.json
pip install markdown
python scripts/generate_equation_implication_js.py /tmp/out.json
- name: Generate the Finite Magma Explorer website
run: |
mkdir -p home_page/fme
cp -r tools/fme/dist/* home_page/fme
~/.elan/bin/lake exe extract_implications unknowns > home_page/fme/unknowns.json
COMMIT_HASH=$(git rev-parse --short HEAD)
sed -i "s/UNKNOWN_VERSION/$COMMIT_HASH/g" home_page/fme/index.html
- name: Bundle dependencies
if: github.event_name == 'push'
uses: ruby/setup-ruby@v1
with:
working-directory: home_page
ruby-version: "3.0" # Specify Ruby version
bundler-cache: true # Enable caching for bundler
- name: Generate home_page/graphiti/graph.json
run: |
~/.elan/bin/lake exe extract_implications --json > /tmp/implications.json
~/.elan/bin/lake exe extract_implications unknowns > /tmp/unknowns.json
ruby scripts/generate_graphiti_data.rb /tmp/implications.json /tmp/unknowns.json data/duals.json > home_page/graphiti/graph.json
- name: Build website using Jekyll
if: github.event_name == 'push' && env.HOME_PAGE_EXISTS == 'true'
working-directory: home_page
run: JEKYLL_ENV=production bundle exec jekyll build # Note this will also copy the blueprint and API doc into home_page/_site
- name: "Upload website (API documentation, blueprint and any home page)"
if: github.event_name == 'push'
uses: actions/upload-pages-artifact@v3
with:
path: ${{ env.HOME_PAGE_EXISTS == 'true' && 'home_page/_site' || 'home_page/' }}
- name: Deploy to GitHub Pages
if: github.event_name == 'push'
id: deployment
uses: actions/deploy-pages@v4
# - name: Make sure the API documentation cache works
# run: mv home_page/docs .lake/build/doc
- name: Remove 'awaiting-CI' label
if: >
always() &&
github.event_name == 'pull_request'
run: |
curl --request DELETE \
--url https://github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels/awaiting-CI \
--header 'authorization: Bearer ${{ secrets.PAT_TOKEN }}' \
--header 'Content-Type: application/json'