[codex] Add finite product quotient layer #74
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
| name: Lean CI | |
| on: | |
| push: | |
| pull_request: | |
| workflow_dispatch: | |
| permissions: {} | |
| concurrency: | |
| group: lean-ci-${{ github.head_ref || github.ref }} | |
| cancel-in-progress: true | |
| env: | |
| ELAN_HOME: /home/runner/.elan | |
| jobs: | |
| # CONTRACT: org ruleset requires this exact check name 'build' | |
| build: | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 120 | |
| permissions: | |
| contents: read | |
| steps: | |
| - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6 | |
| - name: Install elan and toolchain | |
| run: | | |
| curl -sSf https://raw.githubusercontent.com/leanprover/elan/917c18d0ad52f649c2603dc8b973f5b9fa5f8f43/elan-init.sh | sh -s -- -y --default-toolchain none | |
| echo "${ELAN_HOME}/bin" >> "${GITHUB_PATH}" | |
| export PATH="${ELAN_HOME}/bin:${PATH}" | |
| elan --version | |
| elan show | |
| - name: Cache Lake build artifacts | |
| uses: actions/cache@cdf6c1fa76f9f475f3d7449005a359c84ca0f306 # v5.0.3 | |
| with: | |
| path: .lake | |
| key: lake-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json') }} | |
| restore-keys: lake- | |
| - name: Get Mathlib cache | |
| run: lake exe cache get || true | |
| - name: Build (fail on warnings and sorry) | |
| run: make build | |
| - name: Verify theorem dashboard | |
| run: make verify | |
| - name: Check documented theorem names | |
| run: make check-doc-names | |
| - name: Audit for proof placeholders | |
| run: make audit | |
| - name: Lint (Mathlib environment linters) | |
| run: lake lint | |
| - name: Check axiom dashboard for sorry contamination | |
| run: | | |
| echo "Checking axiom dependencies..." | |
| touch OrdvecFormalization/Verify.lean | |
| lake env lean OrdvecFormalization/Verify.lean 2>&1 | tee verify_output.txt | |
| if grep -q "sorryAx" verify_output.txt; then | |
| echo "FATAL: sorryAx found in verified theorems!" | |
| exit 1 | |
| fi | |
| echo "No sorry contamination detected." |