Documentation and planning: Architecture, PaperCodeMapping, PaperMapp… #11
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 4 CI | |
| on: | |
| push: | |
| branches: [ main, develop ] | |
| pull_request: | |
| branches: [ main ] | |
| jobs: | |
| build-and-check: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout repository | |
| uses: actions/checkout@v4 | |
| - name: Install elan | |
| run: | | |
| curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| - name: Install Lean toolchain | |
| run: | | |
| elan toolchain install $(cat lean-toolchain) | |
| elan default $(cat lean-toolchain) | |
| - name: Cache Lake dependencies | |
| uses: actions/cache@v4 | |
| with: | |
| path: .lake | |
| key: ${{ runner.os }}-lake-${{ hashFiles('lakefile.lean', 'lean-toolchain') }} | |
| restore-keys: | | |
| ${{ runner.os }}-lake- | |
| - name: Build production entry | |
| run: | | |
| lake exe cache get || true | |
| lake build Collatz | |
| - name: Proof-chain no-sorry/no-axiom gate | |
| run: | | |
| set -e | |
| CHAIN_FILES=( | |
| "Collatz.lean" | |
| "Collatz/Production.lean" | |
| "Collatz/Foundations/Core.lean" | |
| "Collatz/Epochs/Core.lean" | |
| "Collatz/Epochs/APStructure.lean" | |
| "Collatz/Epochs/Homogenization.lean" | |
| "Collatz/Epochs/NumeratorCarry.lean" | |
| "Collatz/Epochs/LongEpochs.lean" | |
| "Collatz/SEDT/Core.lean" | |
| "Collatz/SEDT/Axioms.lean" | |
| "Collatz/SEDT/Theorems.lean" | |
| "Collatz/Mixing/Semigroup.lean" | |
| "Collatz/Mixing/PhaseMixing.lean" | |
| "Collatz/Mixing/TouchFrequency.lean" | |
| "Collatz/CycleExclusion/CycleDefinition.lean" | |
| "Collatz/CycleExclusion/PeriodSum.lean" | |
| "Collatz/CycleExclusion/PureE1Cycles.lean" | |
| "Collatz/CycleExclusion/MixedCycles.lean" | |
| "Collatz/CycleExclusion/RepeatTrick.lean" | |
| "Collatz/CycleExclusion/Main.lean" | |
| "Collatz/Convergence/Coercivity.lean" | |
| "Collatz/Convergence/FixedPoints.lean" | |
| "Collatz/Convergence/NoAttractors.lean" | |
| "Collatz/Convergence/MainTheorem.lean" | |
| ) | |
| SORRY_COUNT=$(rg -n "\\bsorry\\b" "${CHAIN_FILES[@]}" | wc -l || true) | |
| AXIOM_COUNT=$(rg -n "\\baxiom\\b" "${CHAIN_FILES[@]}" | wc -l || true) | |
| echo "chain_sorry_count=$SORRY_COUNT" >> $GITHUB_ENV | |
| echo "chain_axiom_count=$AXIOM_COUNT" >> $GITHUB_ENV | |
| if [ "$SORRY_COUNT" -ne 0 ]; then | |
| echo "Proof-chain gate failed: found 'sorry'." | |
| rg -n "\\bsorry\\b" "${CHAIN_FILES[@]}" || true | |
| exit 1 | |
| fi | |
| if [ "$AXIOM_COUNT" -ne 0 ]; then | |
| echo "Proof-chain gate failed: found 'axiom'." | |
| rg -n "\\baxiom\\b" "${CHAIN_FILES[@]}" || true | |
| exit 1 | |
| fi | |
| - name: Paper-label mapping gate | |
| run: | | |
| rg -n "D.1|E.2|F.6|F.7|G.5|H.main|I.1" "Collatz/Documentation/PaperCodeMapping.lean" > /dev/null | |
| rg -n "#lem:D1|#thm:E2|#thm:F6|#cor:F7|#thm:G5|#thm:Hmain|#thm:I1" "../collatz-paper/paper/src/md/appendices/internal/INDEX.md" > /dev/null | |
| - name: Generate CI summary | |
| if: always() | |
| run: | | |
| echo "### Lean 4 Proof Closure Summary" >> $GITHUB_STEP_SUMMARY | |
| echo "- chain sorry count: ${chain_sorry_count:-n/a}" >> $GITHUB_STEP_SUMMARY | |
| echo "- chain axiom count: ${chain_axiom_count:-n/a}" >> $GITHUB_STEP_SUMMARY |