Reframe z3py guide intro around Lean as a symbolic reasoning engine (#7) #59
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. | |
| test: | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| os: [ubuntu-latest, macos-latest] | |
| runs-on: ${{ matrix.os }} | |
| 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 | |
| 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 with ASAN via LD_PRELOAD. | |
| # This catches memory errors in our C bridge and ctypes FFI layer | |
| # without needing to rebuild Lean from source. | |
| asan-linux: | |
| runs-on: ubuntu-latest | |
| needs: test | |
| continue-on-error: 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: 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: Run tests under ASAN (LD_PRELOAD) | |
| run: | | |
| LIBASAN=$(gcc -print-file-name=libasan.so) | |
| echo "Using libasan: $LIBASAN" | |
| LEAN_SYSROOT=$(lean --print-prefix) | |
| LD_LIBRARY_PATH="$LEAN_SYSROOT/lib/lean" \ | |
| LD_PRELOAD="$LIBASAN" \ | |
| ASAN_OPTIONS=detect_leaks=0:halt_on_error=1 \ | |
| uv run pytest tests -v --tb=short 2>&1 | tee asan.log | |
| if grep -q "ERROR: AddressSanitizer" asan.log; then | |
| echo "::error::ASAN detected memory errors" | |
| exit 1 | |
| fi | |
| # 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 |