Plan for pinning the GoalState refcount bug via ASAN + rr #13
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: CI | |
| on: [push, pull_request] | |
| jobs: | |
| # Run the full test suite on Linux + macOS across the pinned Lean | |
| # toolchain plus a recent stable and nightly. The lifted Pantograph | |
| # kernel code requires 4.29-era APIs (`String.rawEndPos`, the new | |
| # `Lean.replay` shape, etc.), so we don't try the older 4.25 line. | |
| # `nightly` is allowed to fail — it tracks upstream breakage. | |
| test: | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| os: [ubuntu-latest, macos-latest] | |
| toolchain: | |
| - "default" # what lean-toolchain pins | |
| - "leanprover/lean4:v4.29.1" # latest 4.29 patch release | |
| - "leanprover/lean4:nightly" # tracks main; allowed to fail | |
| include: | |
| - toolchain: "leanprover/lean4:nightly" | |
| allow_failure: true | |
| runs-on: ${{ matrix.os }} | |
| continue-on-error: ${{ matrix.allow_failure == true }} | |
| steps: | |
| - 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: Pick Lean toolchain | |
| id: toolchain | |
| shell: bash | |
| run: | | |
| if [ "${{ matrix.toolchain }}" = "default" ]; then | |
| echo "name=$(cat lean-toolchain)" >> "$GITHUB_OUTPUT" | |
| else | |
| echo "name=${{ matrix.toolchain }}" >> "$GITHUB_OUTPUT" | |
| echo "${{ matrix.toolchain }}" > lean-toolchain | |
| echo "${{ matrix.toolchain }}" > tests/lean/lean-toolchain | |
| fi | |
| - name: Install Lean toolchain | |
| shell: bash | |
| run: | | |
| elan toolchain install ${{ steps.toolchain.outputs.name }} | |
| elan default ${{ steps.toolchain.outputs.name }} | |
| - name: Install uv | |
| uses: astral-sh/setup-uv@v5 | |
| - name: Set up Python | |
| run: uv python install 3.12 | |
| - name: Install Python dependencies | |
| run: uv sync --dev | |
| - name: Install demo dependencies (sympy, numpy) | |
| run: uv pip install sympy numpy | |
| - name: Build root Lake project | |
| run: lake build | |
| - name: Build TestLib (test fixture) | |
| run: lake build TestLib:shared | |
| working-directory: tests/lean | |
| - name: Inspect tests/lean build output (diagnostic) | |
| if: always() | |
| run: | | |
| echo "--- tests/lean/.lake/build ---" | |
| find tests/lean/.lake/build -maxdepth 5 -type f 2>/dev/null | sort | head -50 | |
| echo "------------------------------" | |
| - name: Set library path (for downstream commands) | |
| shell: bash | |
| run: | | |
| LEAN_SYSROOT=$(lean --print-prefix) | |
| if [ "$RUNNER_OS" == "Linux" ]; then | |
| echo "LD_LIBRARY_PATH=$LEAN_SYSROOT/lib/lean" >> $GITHUB_ENV | |
| else | |
| echo "DYLD_LIBRARY_PATH=$LEAN_SYSROOT/lib/lean" >> $GITHUB_ENV | |
| fi | |
| - name: Run tests | |
| run: uv run pytest tests -v | |
| # macOS-only: run the test suite under `leaks` to check for missing | |
| # ref-count drops. This is slower so kept on a separate job. | |
| memory-macos: | |
| runs-on: macos-latest | |
| needs: test | |
| continue-on-error: true # leaks(1) reports of system frameworks are noisy | |
| steps: | |
| - 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: Install uv + deps | |
| uses: astral-sh/setup-uv@v5 | |
| - run: uv python install 3.12 | |
| - run: uv sync --dev | |
| - run: uv pip install sympy numpy | |
| - name: Build | |
| run: | | |
| lake build | |
| (cd tests/lean && lake build) | |
| - name: leaks(1) check | |
| run: tests/leaks_check.sh | |
| # Linux-only: run the test suite under valgrind for stronger coverage | |
| # of definite leaks. | |
| memory-linux: | |
| runs-on: ubuntu-latest | |
| needs: test | |
| continue-on-error: true # valgrind under Python interpreter is noisy | |
| steps: | |
| - 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: Install valgrind | |
| run: | | |
| sudo apt-get update | |
| sudo apt-get install -y valgrind | |
| - name: Install uv + deps | |
| uses: astral-sh/setup-uv@v5 | |
| - run: uv python install 3.12 | |
| - run: uv sync --dev | |
| - run: uv pip install sympy numpy | |
| - name: Build | |
| run: | | |
| lake build | |
| (cd tests/lean && lake build) | |
| - name: valgrind check | |
| run: tests/leaks_check.sh | |
| env: | |
| PYTHONMALLOC: malloc |