chore(deps): bump rmcp from 2.2.0 to 3.1.0 #251
Workflow file for this run
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
| # SPDX-License-Identifier: AGPL-3.0-or-later | |
| # This workflow is managed by gh actions-lock. | |
| name: Idris2 ABI Type-Check | |
| on: | |
| push: | |
| branches: [main] # only post-merge; feature-branch PRs are gated by the pull_request run below | |
| paths: | |
| - 'src/abi/**' | |
| - 'src/idris/**' | |
| - '.github/workflows/idris2-abi-ci.yml' | |
| # No paths-filter on pull_request: this job is a REQUIRED status check, so it | |
| # must report on every PR (a path-filtered required check deadlocks PRs that | |
| # don't touch its paths — they wait forever for a run that never happens). The | |
| # "Detect relevant changes" step below does the path-gating internally instead, | |
| # so the check always reports while heavy work runs only when sources change. | |
| pull_request: | |
| # Cause-B mitigation (#77): cancel superseded runs so stacked pushes | |
| # to the same ref don't pile up identical jobs in the queue. | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| permissions: read-all | |
| jobs: | |
| idris2-typecheck: | |
| name: Type-check Idris2 ABI definitions | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 30 | |
| steps: | |
| - uses: actions/checkout@v7.0.1 | |
| # Required-check shim: decide whether ABI/proof sources actually changed. | |
| # The workflow file itself is intentionally NOT in the pattern, so CI-only | |
| # edits pass through. Non-PR events (push) always run the full check. | |
| - name: Detect relevant changes | |
| id: detect | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| run: | | |
| set -euo pipefail | |
| PATTERN='^(src/abi/|src/idris/)' | |
| if [ "${{ github.event_name }}" = "pull_request" ]; then | |
| FILES=$(gh api "repos/${{ github.repository }}/pulls/${{ github.event.pull_request.number }}/files" \ | |
| --paginate --jq '.[].filename') | |
| if printf '%s\n' "$FILES" | grep -qE "$PATTERN"; then | |
| echo "relevant=true" >> "$GITHUB_OUTPUT" | |
| echo "Idris2 ABI/proof sources changed — running full type-check." | |
| else | |
| echo "relevant=false" >> "$GITHUB_OUTPUT" | |
| echo "No Idris2 source changes — pass-through (required-check shim)." | |
| fi | |
| else | |
| echo "relevant=true" >> "$GITHUB_OUTPUT" | |
| echo "Non-PR event — running full type-check." | |
| fi | |
| - name: Install Idris2 | |
| if: steps.detect.outputs.relevant == 'true' | |
| run: | | |
| # Idris2 v0.8.0 has no pre-built Linux release binary — the | |
| # release-assets array on https://api.github.com/repos/idris-lang/Idris2/releases/tags/v0.8.0 | |
| # is empty, so the legacy `releases/download/.../Linux-x86_64.tar.gz` | |
| # URL returns HTTP 404 and breaks this job on every push. | |
| # Match the live-provers.yml install pattern: prefer the Ubuntu | |
| # 24.04 universe `idris2` package; fall back to a source build | |
| # from the archive tag tarball (the archive API resolves for | |
| # any tag, unlike release-asset URLs). | |
| set -euo pipefail | |
| sudo apt-get update -qq || sudo apt-get update -qq --fix-missing | |
| sudo apt-get install -y --fix-missing idris2 2>/dev/null || { | |
| IDRIS2_VER="v0.8.0" | |
| sudo apt-get install -y --fix-missing chezscheme make libgmp-dev | |
| curl -fsSL --max-time 300 --retry 2 \ | |
| -o /tmp/idris2.tar.gz \ | |
| "https://github.com/idris-lang/Idris2/archive/refs/tags/${IDRIS2_VER}.tar.gz" | |
| mkdir -p /tmp/idris2-src | |
| tar xzf /tmp/idris2.tar.gz -C /tmp/idris2-src --strip-components=1 | |
| (cd /tmp/idris2-src && make bootstrap SCHEME=scheme && sudo make install PREFIX=/usr/local) | |
| } | |
| idris2 --version | |
| - name: Type-check all ABI modules via ipkg | |
| if: steps.detect.outputs.relevant == 'true' | |
| run: | | |
| cd src/abi | |
| echo "=== Type-checking ECHIDNA ABI package (16 modules) ===" | |
| idris2 --build echidnaabi.ipkg | |
| echo "✓ All ABI modules type-check successfully" | |
| - name: Type-check Idris2 proof validator (src/idris) | |
| if: steps.detect.outputs.relevant == 'true' | |
| run: | | |
| # Mirrors `just proofs-idris`. --typecheck (not --build) so no codegen | |
| # backend is required; the declared executable's `main` is exercised | |
| # by `idris2 --build` locally where a backend is present. | |
| cd src/idris | |
| echo "=== Type-checking ECHIDNA proof validator ===" | |
| idris2 --typecheck echidna-validator.ipkg | |
| echo "✓ Validator modules type-check successfully" | |
| - name: Verify no dangerous patterns | |
| if: steps.detect.outputs.relevant == 'true' | |
| run: | | |
| echo "=== Scanning for dangerous patterns in ABI code ===" | |
| FOUND=0 | |
| for pattern in "believe_me" "assert_total" "unsafePerformIO" "prim__crash"; do | |
| if grep -r "$pattern" src/abi/ --include="*.idr"; then | |
| echo "✗ DANGEROUS: Found '$pattern' in ABI code" | |
| FOUND=1 | |
| fi | |
| done | |
| if [ "$FOUND" -eq 0 ]; then | |
| echo "✓ No dangerous patterns found" | |
| else | |
| echo "✗ Dangerous patterns detected — ABI code must be formally verified" | |
| exit 1 | |
| fi | |
| - name: Count modules and report | |
| if: steps.detect.outputs.relevant == 'true' | |
| run: | | |
| echo "=== ABI Module Summary ===" | |
| IDR_COUNT=$(find src/abi -name "*.idr" | wc -l) | |
| echo "Total .idr files: $IDR_COUNT" | |
| echo "" | |
| echo "Module listing:" | |
| find src/abi -name "*.idr" -printf " %P\n" | sort |