fix: Refine Bug 1 - only measure trans_rate when loss < initial/5 #242
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
| # CI workflow for SGC Lean 4 formalization | |
| # Triggers on push to main and pull requests | |
| # Uses leanprover/lean-action for reproducible Lean builds | |
| name: Build | |
| on: | |
| push: | |
| branches: [ main, master, dev, wip-* ] | |
| pull_request: | |
| branches: [ main, master ] | |
| # Cancel in-progress runs for the same branch | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| jobs: | |
| build: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout repository | |
| uses: actions/checkout@v4 | |
| with: | |
| # Disable submodule handling to avoid issues with .lake/packages | |
| submodules: false | |
| - 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: Get Mathlib cache | |
| run: | | |
| # Install lake if needed and get mathlib cache | |
| lake exe cache get || true | |
| - name: Build SGC | |
| run: lake build | |
| - name: Verify no sorries | |
| run: | | |
| set -e | |
| echo "Checking for 'sorry' in source files..." | |
| # Search for sorry as a standalone word (the tactic), excluding: | |
| # - Comment lines (starting with --) | |
| # - Docstrings (/-- ... -/) | |
| # - Backticked references (`sorry`) in documentation | |
| # - Meta-references about verification status | |
| SORRY_COUNT=$(grep -rn --include="*.lean" -E '\bsorry\b' src/ \ | |
| | grep -v '^\s*--' \ | |
| | grep -v '/--' \ | |
| | grep -v '`sorry`' \ | |
| | grep -v 'sorry-free' \ | |
| | grep -v 'zero.*sorry' \ | |
| | grep -v 'unproven' \ | |
| | wc -l || true) | |
| if [ "$SORRY_COUNT" -gt 0 ]; then | |
| echo "Found $SORRY_COUNT potential 'sorry' occurrences:" | |
| grep -rn --include="*.lean" -E '\bsorry\b' src/ \ | |
| | grep -v '^\s*--' \ | |
| | grep -v '/--' \ | |
| | grep -v '`sorry`' \ | |
| | grep -v 'sorry-free' \ | |
| | grep -v 'zero.*sorry' \ | |
| | grep -v 'unproven' || true | |
| # Only fail on main/master branches, warn on dev branches | |
| BRANCH_NAME="${GITHUB_REF#refs/heads/}" | |
| if [[ "$BRANCH_NAME" == "main" || "$BRANCH_NAME" == "master" ]]; then | |
| echo "::error::Sorries not allowed on $BRANCH_NAME branch" | |
| exit 1 | |
| else | |
| echo "::warning::$SORRY_COUNT sorries found - allowed on $BRANCH_NAME branch (WIP)" | |
| fi | |
| else | |
| echo "✓ No active sorries found (verified)" | |
| fi | |
| - name: Post-job Cleanup | |
| if: always() | |
| run: | | |
| echo "Cleaning up build artifacts..." | |
| # 1. Force delete .lake (handle read-only git objects) | |
| if [ -d ".lake" ]; then | |
| chmod -R 777 .lake | |
| rm -rf .lake | |
| echo "✓ .lake directory deleted." | |
| fi | |
| # 2. Remove the .git directory | |
| # This prevents the 'actions/checkout' post-run step from trying | |
| # to scan for submodules in a directory we just confused. | |
| if [ -d ".git" ]; then | |
| rm -rf .git | |
| echo "✓ .git directory deleted (preventing post-job git hooks)." | |
| fi |