diff --git a/.github/workflows/idris2-proof.yml b/.github/workflows/idris2-proof.yml
index 00ac28b..065bf1d 100644
--- a/.github/workflows/idris2-proof.yml
+++ b/.github/workflows/idris2-proof.yml
@@ -65,6 +65,14 @@ jobs:
       - name: Build & install Idris2 ${{ env.IDRIS2_VERSION }}
         run: |
           set -euo pipefail
+          # Build OUTSIDE the checkout. The proof gate sweeps the working tree for
+          # every *.idr and errors on any not in its manifest -- that breadth is
+          # the point (it is why an unlisted proof cannot go unnoticed). The Idris2
+          # source tarball ships hundreds of .idr files under libs/, benchmark/ and
+          # docs/; extracting it into the checkout makes the gate fail on the
+          # compiler's own sources. Keep the tree the gate scans clean.
+          build_dir="$(mktemp -d)"
+          cd "$build_dir"
           tarball="idris2-${IDRIS2_VERSION}.tar.gz"
           curl -fsSL -o "$tarball" \
             "https://codeload.github.com/idris-lang/Idris2/tar.gz/refs/tags/v${IDRIS2_VERSION}"
diff --git a/src/interface/build/ttc/2025081600/Abi/Foreign.ttc b/src/interface/build/ttc/2025081600/Abi/Foreign.ttc
deleted file mode 100644
index e02cc5d..0000000
Binary files a/src/interface/build/ttc/2025081600/Abi/Foreign.ttc and /dev/null differ
diff --git a/src/interface/build/ttc/2025081600/Abi/Foreign.ttm b/src/interface/build/ttc/2025081600/Abi/Foreign.ttm
deleted file mode 100644
index ddb3e35..0000000
Binary files a/src/interface/build/ttc/2025081600/Abi/Foreign.ttm and /dev/null differ
diff --git a/src/interface/build/ttc/2025081600/Abi/Layout.ttc b/src/interface/build/ttc/2025081600/Abi/Layout.ttc
deleted file mode 100644
index 26914fe..0000000
Binary files a/src/interface/build/ttc/2025081600/Abi/Layout.ttc and /dev/null differ
diff --git a/src/interface/build/ttc/2025081600/Abi/Layout.ttm b/src/interface/build/ttc/2025081600/Abi/Layout.ttm
deleted file mode 100644
index ad0f00a..0000000
Binary files a/src/interface/build/ttc/2025081600/Abi/Layout.ttm and /dev/null differ
diff --git a/src/interface/build/ttc/2025081600/Abi/Types.ttc b/src/interface/build/ttc/2025081600/Abi/Types.ttc
deleted file mode 100644
index c201745..0000000
Binary files a/src/interface/build/ttc/2025081600/Abi/Types.ttc and /dev/null differ
diff --git a/src/interface/build/ttc/2025081600/Abi/Types.ttm b/src/interface/build/ttc/2025081600/Abi/Types.ttm
deleted file mode 100644
index 58e96ce..0000000
Binary files a/src/interface/build/ttc/2025081600/Abi/Types.ttm and /dev/null differ