Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 8 additions & 0 deletions .github/workflows/idris2-proof.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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}"
Expand Down
Binary file removed src/interface/build/ttc/2025081600/Abi/Foreign.ttc
Binary file not shown.
Binary file removed src/interface/build/ttc/2025081600/Abi/Foreign.ttm
Binary file not shown.
Binary file removed src/interface/build/ttc/2025081600/Abi/Layout.ttc
Binary file not shown.
Binary file removed src/interface/build/ttc/2025081600/Abi/Layout.ttm
Binary file not shown.
Binary file removed src/interface/build/ttc/2025081600/Abi/Types.ttc
Binary file not shown.
Binary file removed src/interface/build/ttc/2025081600/Abi/Types.ttm
Binary file not shown.
Loading