Fix Lean guard verifier negation parsing #3977
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: | |
| branches: [main] | |
| pull_request: | |
| branches: [main] | |
| types: [opened, synchronize, reopened, edited, labeled, unlabeled] | |
| merge_group: | |
| types: [checks_requested] | |
| workflow_dispatch: | |
| concurrency: | |
| group: ci-${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: ${{ github.event_name == 'pull_request' }} | |
| permissions: | |
| contents: read | |
| jobs: | |
| static: | |
| name: static | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 15 | |
| steps: | |
| - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| persist-credentials: false | |
| - uses: ./.github/actions/setup-python-tests | |
| with: | |
| python-version: "3.12" | |
| - uses: actions/setup-node@820762786026740c76f36085b0efc47a31fe5020 # v7.0.0 | |
| with: | |
| node-version: "24" | |
| package-manager-cache: false | |
| - run: make lint-full | |
| - run: make typecheck | |
| - run: make architecture | |
| - run: make todo-check | |
| - run: make import-contracts | |
| - run: make docs-linkcheck | |
| - run: make deploy-check | |
| - run: make npm-test | |
| - run: make build | |
| - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 | |
| with: | |
| name: dist | |
| path: dist/ | |
| python: | |
| name: python (${{ matrix.lane }}) | |
| runs-on: ubuntu-latest | |
| timeout-minutes: ${{ matrix.timeout-minutes }} | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| include: | |
| - lane: unit | |
| timeout-minutes: 10 | |
| - lane: component | |
| timeout-minutes: 15 | |
| - lane: domain | |
| timeout-minutes: 15 | |
| - lane: provider | |
| timeout-minutes: 25 | |
| - lane: composition | |
| timeout-minutes: 25 | |
| - lane: e2e | |
| timeout-minutes: 15 | |
| steps: | |
| - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| persist-credentials: false | |
| - uses: ./.github/actions/setup-python-tests | |
| with: | |
| python-version: "3.12" | |
| - run: make test-${{ matrix.lane }} | |
| env: | |
| PYTEST_ARGS: >- | |
| --junitxml=pytest.xml | |
| --cov --cov-report= --cov-fail-under=0 | |
| - if: ${{ !cancelled() }} | |
| run: uv cache prune --ci | |
| - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 | |
| if: ${{ !cancelled() }} | |
| with: | |
| name: junit-python-${{ matrix.lane }}-3.12 | |
| path: pytest.xml | |
| if-no-files-found: ignore | |
| retention-days: 7 | |
| - if: ${{ !cancelled() }} | |
| run: mv .coverage .coverage.python-${{ matrix.lane }} | |
| - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 | |
| if: ${{ !cancelled() }} | |
| with: | |
| name: coverage-data-python-${{ matrix.lane }} | |
| path: .coverage.python-${{ matrix.lane }} | |
| include-hidden-files: true | |
| boundaries: | |
| name: boundaries (${{ matrix.lane }}) | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 25 | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| lane: [storage, process, mcp] | |
| steps: | |
| - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| persist-credentials: false | |
| - uses: ./.github/actions/setup-python-tests | |
| with: | |
| python-version: "3.12" | |
| - run: make test-${{ matrix.lane }} | |
| env: | |
| PYTEST_ARGS: >- | |
| --junitxml=pytest.xml | |
| --cov --cov-report= --cov-fail-under=0 | |
| - if: ${{ !cancelled() }} | |
| run: uv cache prune --ci | |
| - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 | |
| if: ${{ !cancelled() }} | |
| with: | |
| name: junit-${{ matrix.lane }}-3.12 | |
| path: pytest.xml | |
| if-no-files-found: ignore | |
| retention-days: 7 | |
| - if: ${{ !cancelled() }} | |
| run: mv .coverage .coverage.${{ matrix.lane }} | |
| - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 | |
| if: ${{ !cancelled() }} | |
| with: | |
| name: coverage-data-${{ matrix.lane }} | |
| path: .coverage.${{ matrix.lane }} | |
| include-hidden-files: true | |
| subprocess_coverage: | |
| name: checker subprocess coverage | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 10 | |
| steps: | |
| - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| persist-credentials: false | |
| - uses: ./.github/actions/setup-python-tests | |
| with: | |
| python-version: "3.12" | |
| - run: make test-checker-subprocess-coverage | |
| - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 | |
| with: | |
| name: coverage-data-checker-subprocess | |
| path: .coverage.checker-subprocess | |
| include-hidden-files: true | |
| wheel: | |
| name: wheel (Python ${{ matrix.python-version }}) | |
| needs: [static] | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 10 | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| python-version: ["3.12", "3.13"] | |
| steps: | |
| - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| persist-credentials: false | |
| - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7.0.0 | |
| with: | |
| python-version: ${{ matrix.python-version }} | |
| - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0 | |
| with: | |
| version: "0.11.28" | |
| - uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1 | |
| with: | |
| name: dist | |
| path: dist | |
| - name: Install and start the built wheel | |
| run: | | |
| wheel="$(find dist -maxdepth 1 -name '*.whl' -print -quit)" | |
| test -n "$wheel" | |
| environment="$RUNNER_TEMP/jacobian-wheel-${{ matrix.python-version }}" | |
| state_dir="$RUNNER_TEMP/jacobian-state-${{ matrix.python-version }}" | |
| uv venv --python "${{ matrix.python-version }}" "$environment" | |
| uv pip install --python "$environment/bin/python" \ | |
| --only-binary :all: "$wheel" | |
| "$environment/bin/jacobian" --help | |
| "$environment/bin/jacobian-mcp" --help | |
| "$environment/bin/jacobian" --state-dir "$state_dir" init | |
| - if: matrix.python-version == '3.13' | |
| uses: ./.github/actions/setup-python-tests | |
| with: | |
| python-version: "3.13" | |
| - if: matrix.python-version == '3.13' | |
| run: make test-compatibility | |
| env: | |
| PYTEST_ARGS: --junitxml=pytest.xml | |
| lean: | |
| name: Lean Runtime | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 30 | |
| steps: | |
| - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| persist-credentials: false | |
| - name: Prepare Lean test environment | |
| uses: ./.github/actions/setup-lean | |
| - run: make test-lean | |
| env: | |
| JACOBIAN_LEAN_REQUIRED: "1" | |
| coverage: | |
| name: Coverage | |
| if: ${{ always() && !cancelled() }} | |
| needs: [python, boundaries, subprocess_coverage] | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 10 | |
| permissions: | |
| contents: read | |
| pull-requests: write | |
| steps: | |
| - name: Require python and boundaries | |
| env: | |
| PYTHON_RESULT: ${{ needs.python.result }} | |
| BOUNDARIES_RESULT: ${{ needs.boundaries.result }} | |
| SUBPROCESS_COVERAGE_RESULT: ${{ needs.subprocess_coverage.result }} | |
| run: | | |
| test "$PYTHON_RESULT" = success | |
| test "$BOUNDARIES_RESULT" = success | |
| test "$SUBPROCESS_COVERAGE_RESULT" = success | |
| - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| persist-credentials: false | |
| - uses: ./.github/actions/setup-python-tests | |
| with: | |
| python-version: "3.12" | |
| - uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1 | |
| with: | |
| pattern: coverage-data-* | |
| path: coverage-data | |
| merge-multiple: true | |
| - run: uv run --locked coverage combine coverage-data | |
| - run: uv run --locked coverage report --fail-under=50 | tee coverage-report.txt | |
| shell: bash -o pipefail {0} | |
| - run: uv run --locked coverage xml | |
| - name: Post coverage summary to PR | |
| if: >- | |
| github.event_name == 'pull_request' && | |
| github.event.pull_request.user.type != 'Bot' && | |
| github.event.pull_request.head.repo.full_name == github.repository | |
| run: | | |
| pct="$(awk '$1 == "TOTAL" { value = $NF; sub(/%$/, "", value); print value }' coverage-report.txt)" | |
| test -n "$pct" | |
| { | |
| echo "<!-- jacobian-coverage-report -->" | |
| echo "## Coverage Report" | |
| echo "" | |
| echo '```' | |
| cat coverage-report.txt | |
| echo '```' | |
| echo "" | |
| echo "**Total coverage: ${pct}%** (threshold: 50%)" | |
| } > coverage-summary.md | |
| jq -n --rawfile body coverage-summary.md '{body: $body}' > coverage-comment.json | |
| list_coverage_comments() { | |
| gh api "repos/$GITHUB_REPOSITORY/issues/$PR_NUMBER/comments" --paginate \ | |
| --jq '.[] | select(.user.login == "github-actions[bot]") | select((.body | contains("<!-- jacobian-coverage-report -->")) or (.body | startswith("## Coverage Report"))) | .id' | |
| } | |
| mapfile -t comment_ids < <(list_coverage_comments) | |
| if [ "${#comment_ids[@]}" -eq 0 ]; then | |
| gh api --method POST \ | |
| "repos/$GITHUB_REPOSITORY/issues/$PR_NUMBER/comments" \ | |
| --input coverage-comment.json | |
| mapfile -t comment_ids < <(list_coverage_comments) | |
| fi | |
| if [ "${#comment_ids[@]}" -eq 0 ]; then | |
| echo "failed to create or locate coverage comment" >&2 | |
| exit 1 | |
| fi | |
| gh api --method PATCH \ | |
| "repos/$GITHUB_REPOSITORY/issues/comments/${comment_ids[0]}" \ | |
| --input coverage-comment.json | |
| for duplicate_id in "${comment_ids[@]:1}"; do | |
| gh api --method DELETE \ | |
| "repos/$GITHUB_REPOSITORY/issues/comments/$duplicate_id" | |
| done | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| PR_NUMBER: ${{ github.event.pull_request.number }} | |
| - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 | |
| with: | |
| name: coverage-3.12 | |
| path: coverage.xml | |
| required: | |
| name: required | |
| if: ${{ always() && !cancelled() }} | |
| needs: [static, python, boundaries, wheel, coverage, lean] | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 5 | |
| steps: | |
| - name: Require static python boundaries wheel coverage and selected specialist lanes | |
| env: | |
| STATIC_RESULT: ${{ needs.static.result }} | |
| PYTHON_RESULT: ${{ needs.python.result }} | |
| BOUNDARIES_RESULT: ${{ needs.boundaries.result }} | |
| WHEEL_RESULT: ${{ needs.wheel.result }} | |
| COVERAGE_RESULT: ${{ needs.coverage.result }} | |
| LEAN_RESULT: ${{ needs.lean.result }} | |
| run: | | |
| test "$STATIC_RESULT" = success | |
| test "$PYTHON_RESULT" = success | |
| test "$BOUNDARIES_RESULT" = success | |
| test "$WHEEL_RESULT" = success | |
| test "$COVERAGE_RESULT" = success | |
| test "$LEAN_RESULT" = success | |
| python-test: | |
| name: Python Tests | |
| if: ${{ always() && !cancelled() }} | |
| needs: [required] | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 5 | |
| steps: | |
| - name: Mirror required for existing branch protection | |
| env: | |
| REQUIRED_RESULT: ${{ needs.required.result }} | |
| run: test "$REQUIRED_RESULT" = success | |
| lean-test: | |
| name: Lean Tests | |
| if: ${{ always() && !cancelled() }} | |
| needs: [lean] | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 5 | |
| steps: | |
| - name: Require Lean on the exact merge candidate | |
| env: | |
| LEAN_RESULT: ${{ needs.lean.result }} | |
| run: test "$LEAN_RESULT" = success | |
| deployment-test: | |
| name: Deployment Tests | |
| if: ${{ always() && !cancelled() }} | |
| needs: [static] | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 5 | |
| steps: | |
| - name: Deploy check runs inside static | |
| env: | |
| STATIC_RESULT: ${{ needs.static.result }} | |
| run: test "$STATIC_RESULT" = success |