Skip to content

Commit c298bc7

Browse files
committed
fix(ci): resolve run.sh tool binaries lazily at their use sites
`resolve_bin ix` ran unconditionally at startup, but bench-main's zkvm-execute job legitimately has no `ix` anywhere: it restores only the `.ixe` cache (REUSE_IXE=1 skips the compile step) and builds its zkVM host via cargo — before the resolve_bin refactor that job never touched `ix` at all, so the eager check regressed it with "ix not found (in-tree or PATH)". Resolve per use site instead: the compile step and the ooc branch resolve `ix`, the aiur branch resolves `bench-typecheck`, and the zkVM branch needs neither.
1 parent 12ff29d commit c298bc7

1 file changed

Lines changed: 5 additions & 2 deletions

File tree

.github/scripts/run.sh

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -104,14 +104,15 @@ esac
104104

105105
# Tool resolution: prefer the in-tree build (so base measures base's code, PR
106106
# the PR's), fall back to PATH — CI restores cached binaries onto PATH instead
107-
# of building in-tree.
107+
# of building in-tree. Resolved LAZILY at each use site: the zkVM branch needs
108+
# neither `ix` nor `bench-typecheck` when REUSE_IXE short-circuits the compile
109+
# (bench-main's zkvm-execute job restores only the `.ixe` cache, no binaries).
108110
resolve_bin() { # <name> → prints the path, or fails
109111
local name="$1" in_tree="$repo/.lake/build/bin/$1"
110112
if [ -x "$in_tree" ]; then printf '%s' "$in_tree"
111113
else command -v "$name" || { echo "::error::$name not found (in-tree or PATH)" >&2; return 2; }
112114
fi
113115
}
114-
ix_bin=$(resolve_bin ix) || exit 2
115116

116117
tmp=$(mktemp -d)
117118
compile_log="$tmp/compile.log"
@@ -121,6 +122,7 @@ ixe="$repo/$benv.ixe"
121122
if [ "${REUSE_IXE:-0}" = 1 ] && [ "$backend" != compile ] && [ -f "$ixe" ]; then
122123
echo "reusing existing $ixe (REUSE_IXE)" >&2
123124
else
125+
ix_bin=$(resolve_bin ix) || exit 2
124126
echo "::group::ix compile $module$benv.ixe ($backend/$mode)"
125127
"$ix_bin" compile "$repo/Benchmarks/Compile/$module.lean" \
126128
--out "$ixe" 2>&1 | tee "$compile_log"
@@ -261,6 +263,7 @@ case "$backend" in
261263
# dependency closure in anon mode — the same mode and scope as the zkVM
262264
# execute above, so the delta isolates in-circuit vs out-of-circuit
263265
# overhead rather than mixing in closure-size or metadata effects.
266+
ix_bin=$(resolve_bin ix) || exit 2
264267
ooc_one() { # <label> <ix-check-args…> → prints one JSON object
265268
local label="$1"; shift
266269
local log="$tmp/n.out"

0 commit comments

Comments
 (0)