Revert "[TEST] Try open LinearAlgebraGame to allow short theorem names" #33
This file contains hidden or 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 # Trigger on pushes to the default branch | |
| 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 | |
| permissions: | |
| contents: read # Read access to repository contents | |
| pages: write # Write access to GitHub Pages | |
| id-token: write # Write access to ID tokens | |
| jobs: | |
| build_project: | |
| runs-on: ubuntu-latest | |
| name: Build project | |
| steps: | |
| - 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: Build project | |
| run: ~/.elan/bin/lake build Game | |
| # API docs cache removed - not building docs in current Lake v4.21.0 setup | |
| # Will need to be re-enabled when doc generation is fixed | |
| # Documentation generation removed - facet no longer supported in Lake v4.21.0 | |
| # This step would previously build API docs but the :docs facet is deprecated | |
| # Keeping as placeholder for future migration to new doc generation system | |
| - name: Skip API documentation (deprecated facet) | |
| run: echo "Skipping API documentation - :docs facet deprecated in Lake v4.21.0" | |
| - name: Check for `home_page` folder # this is meant to detect a Jekyll-based website | |
| 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:20250101 | |
| 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 | |
| export CFLAGS="-I/usr/include/graphviz" | |
| export LDFLAGS="-L/usr/lib/graphviz/" | |
| pip install pygraphviz | |
| 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 | |
| # API documentation copy removed - docs not generated in current Lake v4.21.0 setup | |
| - name: Create placeholder docs directory | |
| run: mkdir -p home_page/docs && echo "API documentation generation pending Lake v4.21.0 migration" > home_page/docs/README.md | |
| - name: Bundle dependencies | |
| 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: Build website using Jekyll | |
| if: 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)" | |
| uses: actions/upload-pages-artifact@v3 | |
| with: | |
| path: ${{ env.HOME_PAGE_EXISTS == 'true' && 'home_page/_site' || 'home_page/' }} | |
| - name: Deploy to GitHub Pages | |
| id: deployment | |
| uses: actions/deploy-pages@v4 | |
| # Cache step removed - API docs not generated in current setup | |
| - name: Skip API documentation cache (docs not generated) | |
| run: echo "Skipping API documentation cache - pending Lake v4.21.0 migration" |