fix(ci): idris-verification install chez symlink for Ubuntu's chezscheme (#122)

* fix(ci): idris-verification install chez symlink for Ubuntu's chezscheme

valence-shell#117 (Idris2 RMO type fixes) blocked on verify-idris2:

  ./bootstrap-stage1-chez.sh: 18: chez: not found
  make: *** [Makefile:256: bootstrap] Error 127

Ubuntu's `chezscheme` apt package installs the binary as `scheme`,
not `chez` — but Idris2's bootstrap-stage1-chex.sh hardcodes the
executable name from $SCHEME. Two equivalent fixes:
  (a) pass SCHEME=scheme to `make bootstrap` instead of SCHEME=chez
  (b) symlink `chez -> scheme`

Picking (b) — keeps SCHEME=chez consistent with the Idris2 README's
canonical bootstrap incantation and lets the rest of the workflow
reference chez directly.

This unblocks #117 (which is the actual proof fix, not a workflow
change) and any future PR touching proofs/idris2/**.

* fix(ci): also symlink chez.boot — Ubuntu ships scheme.boot only

Followup to the chez binary symlink: Chez Scheme picks its boot
file from argv[0], so invoking as `chez` searches for `chez.boot`
which Ubuntu's chezscheme package doesn't ship. It ships:
  /usr/lib/csv9.5.8/ta6le/scheme.boot
  /usr/lib/csv9.5.8/ta6le/petite.boot
  /usr/lib/csv9.5.8/ta6le/chezscheme.boot

So we need both:
  (a) a `chez` binary in PATH       — already done (prior commit)
  (b) a `chez.boot` next to the rest — added here

`dpkg -L chezscheme` locates the boot-file dir version-independently.

Verified locally that boot file lookup at /usr/lib/csv<ver>/ta6le/
is what `cannot find compatible chez.boot in search path` was
hitting. After both symlinks, `chez` should pick up `chez.boot`
and the Idris2 bootstrap completes.

## Why this PR (and not folding into the prior commit)

Already explained in the PR body. This is the same orthogonal CI
infrastructure fix — second half of the same root cause.

## Unblocks

- #117 (proof fix), #123 (equivSym closure) and all future Idris2
  proof PRs validating via the `verify-idris2` oracle.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.github/workflows/idris-verification.yml

@@ -36,6 +36,23 @@ jobs:
         run: |
           sudo apt-get update
           sudo apt-get install -y chezscheme
+          # Ubuntu's chezscheme package installs the binary as `scheme` (not
+          # `chez`) and ships boot files keyed on that name: `scheme.boot`,
+          # `petite.boot`, `chezscheme.boot` at /usr/lib/csv<ver>/<arch>/.
+          # Chez Scheme picks its boot file from argv[0]: a binary invoked
+          # as `chez` searches for `chez.boot`, which Ubuntu does not ship.
+          # So we need BOTH:
+          #   (a) a `chez` binary in PATH, AND
+          #   (b) a matching `chez.boot` next to the other boot files.
+          # Symlinking both keeps SCHEME=chez consistent with upstream docs.
+          if ! command -v chez >/dev/null 2>&1; then
+            sudo ln -s "$(command -v scheme)" /usr/local/bin/chez
+          fi
+          BOOT_DIR=$(dirname "$(dpkg -L chezscheme | grep -m1 'scheme\.boot$')")
+          if [ -n "$BOOT_DIR" ] && [ ! -e "$BOOT_DIR/chez.boot" ]; then
+            sudo ln -s "$BOOT_DIR/scheme.boot" "$BOOT_DIR/chez.boot"
+          fi
+          chez --version || true
 
       - name: Cache Idris2 install
         id: idris2-cache