refactoring fresh generators (#871) #2129
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Compile blueprint | |
| on: | |
| push: | |
| branches: | |
| - main | |
| paths: | |
| - '**/*.lean' | |
| - '**/blueprint.yml' | |
| - 'blueprint/**' | |
| - 'commentary/**' | |
| - 'home_page/**' | |
| - 'tools/fme/**' | |
| - '**/generate_dashboard.py' | |
| - '**/generate_equation_implication_js.py' | |
| - '**/generate_equation_explorer_graph.py' | |
| - '**/generate_graphiti_data.rb' | |
| - 'lean-toolchain' | |
| - 'lakefile.toml' | |
| - 'lake-manifest.json' | |
| pull_request: | |
| branches: | |
| - main | |
| paths: | |
| - '**/*.lean' | |
| - '**/blueprint.yml' | |
| - 'blueprint/**' | |
| - 'commentary/**' | |
| - 'home_page/**' | |
| - 'tools/fme/**' | |
| - '**/generate_dashboard.py' | |
| - '**/generate_equation_implication_js.py' | |
| - '**/generate_equation_explorer_graph.py' | |
| - '**/generate_graphiti_data.rb' | |
| - './scripts/**' | |
| - '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://api.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') }} | |
| #restore-keys: LakeBuild-${{ runner.os }}-${{ hashFiles('lean-toolchain') }} | |
| - 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 equation explorer data | |
| run: | | |
| pip install markdown | |
| python scripts/generate_equation_implication_js.py > home_page/implications/implications.js | |
| ~/.elan/bin/lake exe extract_implications outcomes > /tmp/out.json | |
| ~/.elan/bin/lake exe extract_implications raw --full-entries > /tmp/out2.json | |
| python scripts/generate_equation_explorer_graph.py /tmp/out.json /tmp/out2.json > home_page/implications/graph.json | |
| ~/.elan/bin/lake exe extract_implications outcomes --finite-only > /tmp/out.finite.json | |
| ~/.elan/bin/lake exe extract_implications raw --full-entries --finite-only > /tmp/out2.finite.json | |
| python scripts/generate_equation_explorer_graph.py /tmp/out.finite.json /tmp/out2.finite.json > home_page/implications/finite_graph.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 --finite-only > 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 --only-implications --closure > /tmp/implications.json | |
| ~/.elan/bin/lake exe extract_implications unknowns > /tmp/unknowns.json | |
| ~/.elan/bin/lake exe extract_implications --json --only-implications --closure --finite-only > /tmp/implications.fin.json | |
| ~/.elan/bin/lake exe extract_implications unknowns --finite-only > /tmp/unknowns.fin.json | |
| ruby scripts/generate_graphiti_data.rb data/duals.json /tmp/implications.json /tmp/unknowns.json /tmp/implications.fin.json /tmp/unknowns.fin.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 | |
| env: | |
| JEKYLL_GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| 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://api.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' |