Link formal proof of Beck-Fiala theorem #12704
Workflow file for this run
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 | |
| - '*-webtest' | |
| pull_request: | |
| # The merge queue builds the branch as it will land, so the checks below have | |
| # to report on it or the queue never dequeues anything. | |
| merge_group: | |
| workflow_dispatch: | |
| inputs: | |
| website_only: | |
| description: 'Skip Lean build and use live site data (for website development)' | |
| type: boolean | |
| default: false | |
| permissions: | |
| contents: read | |
| jobs: | |
| # The category check is a policy gate, so it has tests of its own. They need | |
| # no Lean build, so they run alongside it rather than after it. | |
| scripts: | |
| runs-on: ubuntu-latest | |
| name: Test scripts | |
| steps: | |
| - name: Checkout project | |
| uses: actions/checkout@d23441a48e516b6c34aea4fa41551a30e30af803 # v6 | |
| with: | |
| persist-credentials: false | |
| - name: Set up Python | |
| uses: actions/setup-python@ece7cb06caefa5fff74198d8649806c4678c61a1 # v6 | |
| with: | |
| python-version: '3.12.9' | |
| - name: Run script tests | |
| run: python3 -m unittest discover -s scripts -p 'test_*.py' -v | |
| build: | |
| runs-on: ubuntu-latest | |
| name: Build project | |
| steps: | |
| - name: Checkout project | |
| uses: actions/checkout@d23441a48e516b6c34aea4fa41551a30e30af803 # v6 | |
| with: | |
| fetch-depth: 0 | |
| persist-credentials: false | |
| # Two independent halves of this job, each with its own switch. | |
| # | |
| # `website_only` skips the slow Lean compilation and takes the data from | |
| # the live site instead. Triggers: | |
| # - Branches ending in -webtest | |
| # - Manual workflow_dispatch with website_only=true | |
| # | |
| # `site` builds the website and the literate source pages. Rendering the | |
| # literate pages alone takes longer than the Lean build, and a pull | |
| # request cannot deploy the result: the `deploy` job below is restricted | |
| # to `main` and `-webtest` branches. So a pull request skips it, and it | |
| # runs in the merge queue and on `main`, which is where breaking it | |
| # would matter. A pull request that changes the site itself still builds | |
| # it, so the author sees the failure before the queue does. | |
| - name: Detect build mode | |
| id: mode | |
| env: | |
| WEBSITE_ONLY: ${{ inputs.website_only }} | |
| REF_NAME: ${{ github.ref_name }} | |
| EVENT_NAME: ${{ github.event_name }} | |
| run: | | |
| if [[ "$WEBSITE_ONLY" == "true" ]] || \ | |
| [[ "$REF_NAME" == *-webtest ]]; then | |
| echo "website_only=true" >> "$GITHUB_OUTPUT" | |
| echo "::notice::Website-only build: skipping Lean compilation, downloading data from live site." | |
| else | |
| echo "website_only=false" >> "$GITHUB_OUTPUT" | |
| fi | |
| site=true | |
| if [[ "$EVENT_NAME" == "pull_request" ]]; then | |
| # A pull request is checked out as a merge commit, so HEAD^1 is the | |
| # base and this diff is exactly what the pull request changes. If | |
| # that fails for any reason, fall back to building the site. | |
| touched=$(git diff --name-only HEAD^1 HEAD -- \ | |
| site docbuild .github/workflows/build-and-docs.yml 2>/dev/null || echo unknown) | |
| if [[ -z "$touched" ]]; then | |
| site=false | |
| echo "::notice::Pull request leaves the site untouched: validating Lean only." | |
| else | |
| echo "::notice::Pull request touches the site, building it." | |
| fi | |
| fi | |
| echo "site=$site" >> "$GITHUB_OUTPUT" | |
| - name: Install elan | |
| if: steps.mode.outputs.website_only != 'true' | |
| 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: Restore ~/.cache/mathlib | |
| if: steps.mode.outputs.website_only != 'true' | |
| uses: actions/cache/restore@6f8efc29b200d32929f49075959781ed54ec270c # v3 | |
| with: | |
| path: ~/.cache/mathlib | |
| key: oleans-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} | |
| restore-keys: | | |
| oleans-${{ hashFiles('lean-toolchain') }}- | |
| - name: Get olean cache | |
| if: steps.mode.outputs.website_only != 'true' | |
| run: | | |
| lake exe cache unpack | |
| lake exe cache get | |
| - name: Restore local lake build | |
| if: steps.mode.outputs.website_only != 'true' | |
| uses: actions/cache/restore@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 | |
| with: | |
| path: | | |
| .lake/build | |
| docbuild/.lake/build | |
| _literate_html | |
| key: lake-build-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'docbuild/lake-manifest.json', 'docbuild/lakefile.toml') }}-${{ github.sha }} | |
| restore-keys: | | |
| lake-build-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'docbuild/lake-manifest.json', 'docbuild/lakefile.toml') }}- | |
| - name: Generate FormalConjecturesForMathlib.lean | |
| if: steps.mode.outputs.website_only != 'true' | |
| run: | | |
| ./scripts/mk_all_formathlib.sh | |
| # Generating All.lean aggregates all problem files into a single module to detect | |
| # clashing declaration names across problem modules during compilation. | |
| - name: Generate All.lean | |
| if: steps.mode.outputs.website_only != 'true' | |
| run: | | |
| rm -f FormalConjectures/All.lean | |
| lake exe mk_all --lib FormalConjectures || true | |
| mv FormalConjectures.lean FormalConjectures/All.lean | |
| echo "set_option linter.style.moduleDocstring false" >> FormalConjectures/All.lean | |
| - name: Begin Lean problem matcher | |
| if: steps.mode.outputs.website_only != 'true' | |
| uses: leanprover-community/gh-problem-matcher-wrap@65a654fcdf7b64ff7633bc7a558f7b46d59a27bf # master | |
| with: | |
| action: add | |
| linters: lean | |
| - name: Build ForMathlib, utilities, and test | |
| if: steps.mode.outputs.website_only != 'true' | |
| run: | | |
| python3 scripts/lake-build-wrapper.py /tmp/build_summary_formathlib.json lake --wfail build FormalConjecturesForMathlib FormalConjecturesUtil | |
| lake --wfail test | |
| - name: Build problems | |
| if: steps.mode.outputs.website_only != 'true' | |
| run: | | |
| python3 scripts/lake-build-wrapper.py /tmp/build_summary_problems.json lake --wfail build | |
| rm -f FormalConjectures/All.lean | |
| - name: End Lean problem matcher | |
| if: always() && steps.mode.outputs.website_only != 'true' | |
| uses: leanprover-community/gh-problem-matcher-wrap@65a654fcdf7b64ff7633bc7a558f7b46d59a27bf # master | |
| with: | |
| action: remove | |
| linters: lean | |
| - name: Build literate source pages | |
| if: steps.mode.outputs.website_only != 'true' && steps.mode.outputs.site == 'true' | |
| run: | | |
| cd docbuild | |
| lake build FormalConjectures:literate | |
| lake exe verso-html .lake/build/literate ../_literate_html | |
| - name: Post-process literate HTML | |
| if: steps.mode.outputs.website_only != 'true' && steps.mode.outputs.site == 'true' | |
| run: | | |
| python3 site/fix_literate_html.py _literate_html | |
| - name: Save local lake build | |
| if: steps.mode.outputs.website_only != 'true' && github.event_name == 'push' | |
| uses: actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 | |
| with: | |
| path: | | |
| .lake/build | |
| docbuild/.lake/build | |
| _literate_html | |
| key: lake-build-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'docbuild/lake-manifest.json', 'docbuild/lakefile.toml') }}-${{ github.sha }} | |
| # Only a push writes to the shared cache. An entry saved from anywhere | |
| # else is scoped to a ref nothing later restores from, while it takes | |
| # 0.37 GB of a 10 GB repository budget that is currently full, evicting | |
| # the `main` entries every build falls back to through `restore-keys`. | |
| # A pull request entry is visible only to that pull request's own later | |
| # runs. A merge queue entry is worse: `gh-readonly-queue/...` is deleted | |
| # as soon as the batch merges, so the entry is unreachable the moment it | |
| # is written. | |
| - name: Pack olean cache | |
| if: steps.mode.outputs.website_only != 'true' && github.event_name == 'push' | |
| run: | | |
| lake exe cache pack | |
| ls ~/.cache/mathlib | |
| - name: Save ~/.cache/mathlib | |
| if: steps.mode.outputs.website_only != 'true' && github.event_name == 'push' | |
| uses: actions/cache/save@6f8efc29b200d32929f49075959781ed54ec270c # v3 | |
| with: | |
| path: ~/.cache/mathlib | |
| key: oleans-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} | |
| - name: Set up Python | |
| if: steps.mode.outputs.website_only != 'true' | |
| uses: actions/setup-python@ece7cb06caefa5fff74198d8649806c4678c61a1 # v6 | |
| with: | |
| python-version: '3.12.9' | |
| # Only the plotting and Verso-fragment scripts need these; the category | |
| # check below is standard library only. | |
| - name: Install Python dependencies | |
| if: steps.mode.outputs.website_only != 'true' && steps.mode.outputs.site == 'true' | |
| run: | | |
| python -m pip install --upgrade pip | |
| pip install pandas==2.2.3 numpy==2.2.3 plotly==5.20.0 beautifulsoup4 lxml | |
| - name: Run plotting script | |
| if: steps.mode.outputs.website_only != 'true' && steps.mode.outputs.site == 'true' | |
| run: | | |
| mkdir -p site/data | |
| python site/plot_growth.py | |
| - name: Set up Node.js | |
| if: steps.mode.outputs.site == 'true' | |
| uses: actions/setup-node@49933ea5288caeca8642d1e84afbd3f7d6820020 # v4 | |
| with: | |
| node-version: '18' | |
| - name: Generate conjectures data for website | |
| if: steps.mode.outputs.website_only != 'true' | |
| run: | | |
| mkdir -p site/data | |
| lake exe extract_names --exclude=statement,docstring,moduleDocstrings,fileFirstAdded,fileLastModified \ | |
| > site/data/conjectures.json | |
| # `extract_names` notices `research open` problems with a sorry-free proof, | |
| # and `test`/`API` statements without one, all decidable from the JSON just | |
| # written. The first is a contradiction and fails; the other two are counted | |
| # in the run summary without blocking. | |
| - name: Check category warnings | |
| if: steps.mode.outputs.website_only != 'true' | |
| run: python3 scripts/check_category_warnings.py site/data/conjectures.json | |
| - name: Extract Verso fragments for website | |
| if: steps.mode.outputs.website_only != 'true' && steps.mode.outputs.site == 'true' | |
| run: | | |
| python3 site/extract_verso_fragments.py _literate_html site/data/verso-fragments.json | |
| # In website-only mode, download data from the live production site | |
| # instead of building it from scratch. The live site serves the processed | |
| # format ({ conjectures, versoFragments, ... }), so we convert it back to | |
| # the raw extract_names format ({ problems }) that build.js expects. | |
| - name: Download live site data | |
| if: steps.mode.outputs.website_only == 'true' | |
| run: | | |
| LIVE_URL="https://google-deepmind.github.io/formal-conjectures" | |
| mkdir -p site/data _literate_html | |
| echo "Downloading conjectures data from $LIVE_URL ..." | |
| curl -sfL "$LIVE_URL/data/conjectures.json" -o /tmp/live_conjectures.json | |
| echo "Downloading growth plots from $LIVE_URL ..." | |
| curl -sfL "$LIVE_URL/data/file_counts_white.html" -o site/data/file_counts_white.html || true | |
| curl -sfL "$LIVE_URL/data/file_counts_dark.html" -o site/data/file_counts_dark.html || true | |
| node -e " | |
| const fs = require('fs'); | |
| const data = JSON.parse(fs.readFileSync('/tmp/live_conjectures.json', 'utf8')); | |
| // Convert processed conjectures back to raw extract_names format | |
| const problems = (data.conjectures || []).map(c => ({ | |
| theorem: c.theorem, | |
| module: c.module, | |
| category: c.category, | |
| subjects: (c.subjects || []).map(s => | |
| typeof s === 'object' ? s.code : s | |
| ), | |
| formalProofs: c.formalProofs || [], | |
| hasSorryFreeProof: false, | |
| })); | |
| fs.writeFileSync( | |
| 'site/data/conjectures.json', | |
| JSON.stringify({ problems }) | |
| ); | |
| // Extract Verso fragments if present | |
| if (data.versoFragments) { | |
| fs.writeFileSync( | |
| 'site/data/verso-fragments.json', | |
| JSON.stringify(data.versoFragments) | |
| ); | |
| } | |
| console.log('Converted ' + problems.length + ' conjectures to raw format.'); | |
| " | |
| - name: Build website | |
| if: steps.mode.outputs.site == 'true' | |
| run: | | |
| cd site | |
| node build.js | |
| env: | |
| BASE_PATH: /formal-conjectures | |
| GITHUB_TOKEN: ${{ github.token }} | |
| - name: Assemble deploy artifact | |
| if: steps.mode.outputs.site == 'true' | |
| run: | | |
| mkdir -p _deploy | |
| # Website goes at root | |
| cp -r site/site/* _deploy/ | |
| # Literate source pages go under /src (may not exist in website-only mode) | |
| if [[ -d _literate_html ]] && [[ -n "$(ls -A _literate_html 2>/dev/null)" ]]; then | |
| cp -r _literate_html _deploy/src | |
| fi | |
| - name: Upload deploy artifact | |
| id: deployment | |
| if: steps.mode.outputs.site == 'true' | |
| uses: actions/upload-pages-artifact@7b1f4a764d45c48632c6b24a0339c27f5614fb0b # v4 | |
| with: | |
| path: _deploy | |
| # Deployment job | |
| deploy: | |
| if: >- | |
| github.ref == 'refs/heads/main' || | |
| (github.repository != 'google-deepmind/formal-conjectures' && | |
| endsWith(github.ref_name, '-webtest')) | |
| environment: | |
| name: github-pages | |
| url: ${{ steps.deployment.outputs.page_url }} | |
| runs-on: ubuntu-latest | |
| needs: build | |
| # Only the deployment job needs write access to Pages and the OIDC token. | |
| permissions: | |
| contents: read | |
| pages: write | |
| id-token: write | |
| steps: | |
| - name: Deploy to GitHub Pages | |
| id: deployment | |
| uses: actions/deploy-pages@d6db90164ac5ed86f2b6aed7e0febac5b3c0c03e # v4 |