Skip to content

Commit 03e7935

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
feat(ci): add Idris2 build oracle — Justfile recipes + verify workflow (closes #70) (#106)
Adds the missing Idris2 layer build oracle. Previously the Idris2 proof tree had no canonical truth check: no Justfile target, no CI workflow, and a typical Idris2 0.8.0 install ships stdlib TTC without source, defeating ad-hoc `idris2 --install` recipes. Justfile - `build-idris2` runs `idris2 --build valence-shell.ipkg` from `proofs/idris2/`. - `verify-idris2` extends `build-idris2` with a hole-count regression signal. - `build-all` updated to include `build-idris2`. - `help` entries added. CI workflow `.github/workflows/idris-verification.yml` - Mirrors `validation.yml`'s `verify-proofs` (Coq) and `lean-verification.yml`'s structure. - Builds Idris2 0.8.0 from source on first run; caches `~/.idris2` for subsequent runs (`make bootstrap SCHEME=chez && make install && make install-libs`). - Captures build log, surfaces hole count + build status to job summary, uploads log as artifact. - Non-blocking until pre-existing parse/typecheck issues at `hardwareEraseIrreversible` + `Composition.idr` clear (tracked by #94). Final `exit 0` flips to `exit 1` when ready to gate. README - Documents the build oracle and the current known-failing status, with pointers to the pre-existing debt tracked in #94. Closes #70. Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 51a81aa commit 03e7935

3 files changed

Lines changed: 163 additions & 1 deletion

File tree

‎.github/workflows/idris-verification.yml‎

Lines changed: 121 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,121 @@
1+
# SPDX-License-Identifier: MPL-2.0
2+
name: Idris2 Verification Build
3+
4+
# Idris2 build oracle for proofs/idris2/. Mirrors the Coq verify-proofs job in
5+
# validation.yml and the lean-verification.yml structure. Closes #70.
6+
#
7+
# Strategy: build Idris2 0.8.0 from source on first run, cache the install for
8+
# subsequent runs. Runs `idris2 --build valence-shell.ipkg` against the ipkg
9+
# manifest. Hole inventory is surfaced to the job summary as a regression signal
10+
# (not a gate — holes are tracked as honest debt; see #94).
11+
12+
on:
13+
push:
14+
branches: [main]
15+
paths:
16+
- 'proofs/idris2/**'
17+
- '.github/workflows/idris-verification.yml'
18+
pull_request:
19+
paths:
20+
- 'proofs/idris2/**'
21+
- '.github/workflows/idris-verification.yml'
22+
workflow_dispatch:
23+
24+
permissions:
25+
contents: read
26+
27+
jobs:
28+
verify-idris2:
29+
name: verify-idris2 (Idris2 build oracle)
30+
runs-on: ubuntu-latest
31+
32+
steps:
33+
- uses: actions/checkout@1cce3390c2bfda521930d01229c073c7ff920824 # v4
34+
35+
- name: Install Chez Scheme (Idris2 runtime dependency)
36+
run: |
37+
sudo apt-get update
38+
sudo apt-get install -y chezscheme
39+
40+
- name: Cache Idris2 install
41+
id: idris2-cache
42+
uses: actions/cache@27d5ce7f107fe9357f9df03efb73ab90386fccae # v4
43+
with:
44+
path: ~/.idris2
45+
key: idris2-0.8.0-${{ runner.os }}-v1
46+
47+
- name: Build Idris2 0.8.0 from source
48+
if: steps.idris2-cache.outputs.cache-hit != 'true'
49+
run: |
50+
# v0.8.0 release tag. Bootstrap via Chez Scheme — the only fully-
51+
# supported backend for self-hosting per upstream README.
52+
git clone --branch v0.8.0 --depth 1 https://github.com/idris-lang/Idris2.git /tmp/idris2-src
53+
cd /tmp/idris2-src
54+
make bootstrap SCHEME=chez
55+
make install
56+
# Install the stdlib packages bundled with the source tree. These
57+
# are required by valence-shell.ipkg's `depends = base, contrib`.
58+
make install-libs
59+
60+
- name: Configure PATH + IDRIS2_PREFIX
61+
run: |
62+
echo "$HOME/.idris2/bin" >> $GITHUB_PATH
63+
echo "IDRIS2_PREFIX=$HOME/.idris2" >> $GITHUB_ENV
64+
65+
- name: Show Idris2 version
66+
run: idris2 --version
67+
68+
- name: List installed Idris2 packages
69+
run: idris2 --list-packages
70+
71+
- name: Build Idris2 proofs (oracle)
72+
id: idris2-build
73+
working-directory: proofs/idris2
74+
run: |
75+
set +e
76+
idris2 --build valence-shell.ipkg 2>&1 | tee idris2-build.log
77+
echo "build_exit=${PIPESTATUS[0]}" >> $GITHUB_OUTPUT
78+
# Surface result without failing the step — the post-step explicitly
79+
# decides gate behaviour. Allows hole inventory to always run.
80+
exit 0
81+
82+
- name: Idris2 hole inventory
83+
if: always()
84+
working-directory: proofs/idris2
85+
run: |
86+
echo "## Idris2 build oracle (#70)" >> $GITHUB_STEP_SUMMARY
87+
echo "" >> $GITHUB_STEP_SUMMARY
88+
# Holes are Idris2 `?identifier` lexemes. Count distinct names.
89+
holes=$(grep -rohE "\\?[a-zA-Z_][a-zA-Z0-9_']*" src/ 2>/dev/null | sort -u | wc -l)
90+
echo "Distinct \`?holes\`: **$holes**" >> $GITHUB_STEP_SUMMARY
91+
echo "" >> $GITHUB_STEP_SUMMARY
92+
if [[ "${{ steps.idris2-build.outputs.build_exit }}" == "0" ]]; then
93+
echo "Build status: **PASS**" >> $GITHUB_STEP_SUMMARY
94+
else
95+
echo "Build status: **FAIL** (exit ${{ steps.idris2-build.outputs.build_exit }})" >> $GITHUB_STEP_SUMMARY
96+
echo "" >> $GITHUB_STEP_SUMMARY
97+
echo "See pre-existing debt in #94 (10 Idris2 partial markers + Model.idr/RMO.idr/Composition.idr typecheck gaps)." >> $GITHUB_STEP_SUMMARY
98+
fi
99+
echo "" >> $GITHUB_STEP_SUMMARY
100+
echo "<details><summary>Build log (last 60 lines)</summary>" >> $GITHUB_STEP_SUMMARY
101+
echo "" >> $GITHUB_STEP_SUMMARY
102+
echo '```' >> $GITHUB_STEP_SUMMARY
103+
tail -60 idris2-build.log >> $GITHUB_STEP_SUMMARY
104+
echo '```' >> $GITHUB_STEP_SUMMARY
105+
echo "</details>" >> $GITHUB_STEP_SUMMARY
106+
107+
- name: Upload build log
108+
if: always()
109+
uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7
110+
with:
111+
name: idris2-build-log
112+
path: proofs/idris2/idris2-build.log
113+
114+
- name: Gate on build status
115+
if: steps.idris2-build.outputs.build_exit != '0'
116+
run: |
117+
echo "::warning::Idris2 build oracle FAILED (exit ${{ steps.idris2-build.outputs.build_exit }}). Tracked as pre-existing debt in #94."
118+
# Non-blocking by default. To make this a required gate once pre-
119+
# existing issues are fixed, change `exit 0` to `exit 1` below and
120+
# add to branch protection's required checks list.
121+
exit 0

‎Justfile‎

Lines changed: 19 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ default:
88
@just --list
99

1010
# Build all proofs across all systems
11-
build-all: build-coq build-lean4 build-agda build-isabelle build-mizar
11+
build-all: build-coq build-lean4 build-agda build-isabelle build-mizar build-idris2
1212
@echo "✓ All proofs built"
1313

1414
# Verify all proofs
@@ -50,6 +50,22 @@ build-mizar:
5050
cd proofs/mizar && mizf filesystem_model.miz || echo "⚠ Mizar not configured"
5151
cd proofs/mizar && mizf file_operations.miz || echo "⚠ Mizar not configured"
5252

53+
# Requires Idris2 0.8.0. Install via:
54+
# nix-shell -p idris2 # recommended for reproducibility
55+
# asdf install idris2 latest
56+
# or build from source at https://github.com/idris-lang/Idris2
57+
# Build Idris2 proofs (oracle — see .github/workflows/idris-verification.yml)
58+
build-idris2:
59+
@echo "Building Idris2 proofs..."
60+
cd proofs/idris2 && idris2 --build valence-shell.ipkg
61+
@echo "✓ Idris2 proofs type-checked"
62+
63+
# Verify Idris2: build then count remaining ?holes (regression signal).
64+
verify-idris2: build-idris2
65+
@echo "Counting Idris2 holes..."
66+
@holes=$$(grep -rohE "\\?[a-zA-Z_][a-zA-Z0-9_']*" proofs/idris2/src/ 2>/dev/null | sort -u | wc -l); \
67+
echo " Distinct holes: $$holes"
68+
5369
# Extract Coq to OCaml
5470
extract:
5571
@echo "Extracting Coq to OCaml..."
@@ -374,6 +390,8 @@ help:
374390
@echo " just build-agda - Build Agda proofs"
375391
@echo " just build-isabelle - Build Isabelle proofs"
376392
@echo " just build-mizar - Build Mizar proofs"
393+
@echo " just build-idris2 - Build Idris2 proofs"
394+
@echo " just verify-idris2 - Build + hole-count Idris2 proofs"
377395
@echo ""
378396
@echo "Testing:"
379397
@echo " just test-ffi-zig - Test Zig FFI"

‎proofs/idris2/README.md‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -94,6 +94,29 @@ idris2 --build valence-shell.ipkg
9494
idris2 --codegen chez --output vsh-core src/Main.idr
9595
```
9696

97+
### Build oracle (Justfile)
98+
99+
The `build-idris2` and `verify-idris2` recipes in the top-level `Justfile`
100+
wrap the above. They are mirrored by the `idris-verification.yml` CI job.
101+
102+
```bash
103+
# From repo root:
104+
just build-idris2 # cd proofs/idris2 && idris2 --build valence-shell.ipkg
105+
just verify-idris2 # build + count distinct ?holes for regression tracking
106+
```
107+
108+
#### Known oracle status (2026-06-01)
109+
110+
`build-idris2` currently fails on pre-existing issues outside #60/#61's scope:
111+
112+
- `Filesystem/Model.idr` — `equivSym` / `equivTrans` are deliberate `?holes`; trivial closure when needed.
113+
- `Filesystem/RMO.idr` — `hardwareEraseIrreversible`'s `() -> Filesystem` parameter has a parse issue under Idris2 0.8.0 (tracked as part of #94 alongside the 10 partial markers).
114+
- `Filesystem/Composition.idr` — multiple holes pending Coq/Lean port.
115+
116+
The CI job is configured non-blocking until the pre-existing parse/typecheck
117+
issues land. Once green, flip the final `exit 0` in `idris-verification.yml`
118+
to `exit 1` and add the job to branch protection's required checks.
119+
97120
### Run Tests
98121

99122
```bash

0 commit comments

Comments
 (0)