Add Catch-Up game conjecture #2975
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
| # Copyright 2025 The Formal Conjectures Authors. | |
| # Licensed under the Apache License, Version 2.0 (the "License"); | |
| # you may not use this file except in compliance with the License. | |
| # You may obtain a copy of the License at | |
| # https://www.apache.org/licenses/LICENSE-2.0 | |
| # Unless required by applicable law or agreed to in writing, software | |
| # distributed under the License is distributed on an "AS IS" BASIS, | |
| # WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. | |
| # See the License for the specific language governing permissions and | |
| # limitations under the License. | |
| name: Build Lean project and deploy docs | |
| on: | |
| push: | |
| branches: | |
| - main | |
| pull_request: | |
| # Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages | |
| permissions: | |
| contents: read | |
| pages: write | |
| id-token: write | |
| jobs: | |
| build: | |
| runs-on: ubuntu-latest | |
| name: Build project | |
| steps: | |
| - name: Checkout project | |
| uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 0 | |
| - name: Install elan | |
| run: | | |
| set -o pipefail | |
| curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz | |
| ./elan-init -y --default-toolchain none | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| - name: Generate All.lean | |
| run: | | |
| lake exe mk_all --lib FormalConjectures || true | |
| # Avoid including Test files from `Util/` to avoid inflating the | |
| # stats. This stop-gap should be removed after doing the TODO at | |
| # `fetchStatsMarkdown` in `docbuild/overwrite-index.lean`. | |
| grep -v "FormalConjectures\.Util\." FormalConjectures.lean > FormalConjectures/All.lean | |
| - name: Restore ~/.cache/mathlib | |
| uses: actions/cache/restore@v3 | |
| with: | |
| path: ~/.cache/mathlib | |
| key: oleans-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('**/*.lean') }} | |
| restore-keys: | | |
| oleans-${{ hashFiles('lake-manifest.json') }}- | |
| oleans- | |
| - name: Get olean cache | |
| run: | | |
| lake exe cache unpack | |
| lake exe cache get | |
| - name: Build project | |
| run: | | |
| lake build | |
| - name: Pack olean cache | |
| run: | | |
| lake exe cache pack | |
| ls ~/.cache/mathlib | |
| - name: Save ~/.cache/mathlib | |
| uses: actions/cache/save@v3 | |
| with: | |
| path: ~/.cache | |
| key: oleans-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('**/*.lean') }} | |
| - name: Prepare documentation | |
| run: | | |
| cd docbuild | |
| export MATHLIB_NO_CACHE_ON_UPDATE=1 # avoids "Failed to prune ProofWidgets cloud release: no such file or directory" | |
| lake update formal_conjectures | |
| - name: Cache documentation | |
| uses: actions/cache@v4 | |
| with: | |
| path: docbuild/.lake/build/doc | |
| key: MathlibDoc-${{ hashFiles('docbuild/lake-manifest.json') }}-${{ hashFiles('**/*.lean') }} | |
| restore-keys: | | |
| MathlibDoc-${{ hashFiles('docbuild/lake-manifest.json') }}- | |
| MathlibDoc- | |
| - name: Build documentation | |
| run: | | |
| cd docbuild | |
| lake build FormalConjectures:docs | |
| - name: Extract documentation | |
| run: | | |
| cd docbuild | |
| mkdir out | |
| lake query FormalConjectures:docs > out-files.txt | |
| sed -i 's|^.*\.lake/build/doc/||' out-files.txt | |
| echo "::group::Generated files" | |
| cat out-files.txt | |
| echo "::endgroup::" | |
| rsync -a --files-from=out-files.txt --relative .lake/build/doc ./out | |
| - name: Set up Python | |
| uses: actions/setup-python@v5 | |
| with: | |
| python-version: '3.12.9' | |
| - name: Install Python dependencies | |
| run: | | |
| python -m pip install --upgrade pip | |
| pip install pandas==2.2.3 numpy==2.2.3 plotly==5.20.0 | |
| - name: Run plotting script | |
| run: | | |
| python docbuild/scripts/plot_growth.py | |
| - name: Inject stats into index.html | |
| shell: bash | |
| run: | | |
| cd docbuild | |
| lake exe overwrite_index ./out/index.html ./out/file_counts.html | tee -a "$GITHUB_STEP_SUMMARY" | |
| - name: Upload docs | |
| id: deployment | |
| uses: actions/upload-pages-artifact@v3 | |
| with: | |
| path: docbuild/out | |
| # Deployment job | |
| deploy: | |
| if: github.ref == 'refs/heads/main' | |
| environment: | |
| name: github-pages | |
| url: ${{ steps.deployment.outputs.page_url }} | |
| runs-on: ubuntu-latest | |
| needs: build | |
| steps: | |
| - name: Deploy to GitHub Pages | |
| id: deployment | |
| uses: actions/deploy-pages@v4 |