Merge pull request #1 from ejgallego/fix-ci-install-shell-lint

Fix install CI checks

Author: ejgallego

.github/workflows/ci.yml

@@ -6,6 +6,8 @@ name: CI
 
 on:
   push:
+    branches:
+      - main
   pull_request:
 
 permissions:
@@ -57,3 +59,47 @@ jobs:
 
       - name: Broker Slow Test
         run: bash tests/test-broker-slow.sh
+
+  install:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - uses: ./.github/actions/lean-ci-setup
+
+      - name: Install Test
+        run: bash tests/test-install.sh
+
+  toolchain-compat:
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        toolchain:
+          - leanprover/lean4:v4.29.0-rc6
+          - leanprover/lean4:v4.29.0-rc5
+    steps:
+      - uses: actions/checkout@v4
+
+      - uses: ./.github/actions/lean-ci-setup
+
+      - name: Validate toolchain compatibility
+        run: bash tests/test-toolchain-compat.sh '${{ matrix.toolchain }}'
+
+  broker-rocq:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - uses: ./.github/actions/lean-ci-setup
+
+      - name: Set up OCaml / opam
+        uses: ocaml/setup-ocaml@v3
+        with:
+          ocaml-compiler: 4.14.2
+
+      - name: Install Rocq Tooling
+        run: bash tests/setup-rocq-opam.sh
+
+      - name: Broker Rocq Test
+        run: bash tests/test-broker-rocq.sh

scripts/install-beam.sh

@@ -289,9 +289,7 @@ hash_tool() {
 }
 
 read_supported_toolchains() {
-  local output_name="$1"
-  local -n output_ref="$output_name"
-  mapfile -t output_ref < <("$beam_cli" supported-toolchains lean)
+  "$beam_cli" supported-toolchains lean
 }
 
 array_contains() {
@@ -308,8 +306,6 @@ array_contains() {
 
 resolve_install_toolchains() {
   local repo_toolchain="$1"
-  local output_name="$2"
-  local -n output_ref="$output_name"
   local supported_toolchains=()
   local selected=()
   local toolchain=""
@@ -318,7 +314,7 @@ resolve_install_toolchains() {
     die "cannot combine --all-supported with --toolchain"
   fi
 
-  read_supported_toolchains supported_toolchains
+  mapfile -t supported_toolchains < <(read_supported_toolchains)
   if [ "${#supported_toolchains[@]}" -eq 0 ]; then
     die "beam CLI reported no supported Lean toolchains"
   fi
@@ -341,7 +337,7 @@ resolve_install_toolchains() {
     selected=("$repo_toolchain")
   fi
 
-  output_ref=("${selected[@]}")
+  printf '%s\n' "${selected[@]}"
 }
 
 hash_tree() {
@@ -402,12 +398,11 @@ stage_runtime_tree() {
   local dest="$1"
   local entry=""
   local mode=""
-  local manifest_group=""
   local src_rel=""
   local dest_rel=""
   mkdir -p "$dest"
   for entry in "${runtime_payload_spec[@]}"; do
-    IFS='|' read -r mode manifest_group src_rel dest_rel <<< "$entry"
+    IFS='|' read -r mode _ src_rel dest_rel <<< "$entry"
     case "$mode" in
       copy)
         copy_repo_path_if_present "$repo_root/$src_rel" "$dest/$dest_rel" "$dest"
@@ -471,12 +466,19 @@ prepare_install_environment() {
   local toolchain_name="$1"
   local selected_name="$2"
   local -n toolchain_ref="$toolchain_name"
-  local -n selected_ref="$selected_name"
+  local -n selected_toolchains_ref="$selected_name"
+  local resolved_toolchains=""
   require_elan
   toolchain_ref="$(awk 'NR==1 {print $1}' "$repo_root/lean-toolchain")"
   require_repo_toolchain "$toolchain_ref"
   ensure_runtime_artifacts
-  resolve_install_toolchains "$toolchain_ref" selected_ref
+  resolved_toolchains="$(resolve_install_toolchains "$toolchain_ref")"
+  # shellcheck disable=SC2034
+  if [ -n "$resolved_toolchains" ]; then
+    mapfile -t selected_toolchains_ref <<< "$resolved_toolchains"
+  else
+    selected_toolchains_ref=()
+  fi
   verify_publish_targets
   mkdir -p "$bin_home" "$versions_root" "$state_root"
 }

supported-lean-toolchains

@@ -1,2 +1,3 @@
 # Validated Lean toolchains that beam is willing to serve.
 leanprover/lean4:v4.29.0-rc6
+leanprover/lean4:v4.29.0-rc5

tests/test-broker-rocq.sh

@@ -0,0 +1,40 @@
+#!/usr/bin/env bash
+
+# Copyright (c) 2026 Lean FRO LLC. All rights reserved.
+# Released under Apache 2.0 license as described in the file LICENSE.
+# Author: Emilio J. Gallego Arias
+
+set -euo pipefail
+
+cd "$(dirname "$0")/.."
+
+echo "[broker-rocq] build"
+lake build \
+  beam-cli \
+  beam-daemon \
+  beam-client \
+  beam-daemon-rocq-smoke-test \
+  > /dev/null
+
+ROCQ_LSP=""
+for candidate in "_opam/bin/coq-lsp" "_opam/_opam/bin/coq-lsp"; do
+  if [ -x "$candidate" ]; then
+    ROCQ_LSP="$candidate"
+    break
+  fi
+done
+
+if [ -z "$ROCQ_LSP" ]; then
+  echo "missing coq-lsp; run tests/setup-rocq-opam.sh first" >&2
+  exit 1
+fi
+
+if [ -d "_opam/_opam" ]; then
+  eval "$(opam env --switch=./_opam --set-switch)"
+fi
+
+echo "[broker-rocq] wrapper tests"
+BEAM_ROCQ_CMD="$PWD/$ROCQ_LSP" bash tests/test-beam-wrapper-rocq.sh > /dev/null
+
+echo "[broker-rocq] smoke test"
+BEAM_ROCQ_CMD="$PWD/$ROCQ_LSP" .lake/build/bin/beam-daemon-rocq-smoke-test > /dev/null

tests/test-broker-slow.sh

@@ -44,7 +44,6 @@ lake build \
   beam-cli \
   beam-daemon \
   beam-client \
-  beam-daemon-rocq-smoke-test \
   > /dev/null
 
 echo "[broker-slow] bundle install"
@@ -54,29 +53,6 @@ echo "[broker-slow] wrapper tests"
 HOME="$tmp_env_root/home" CODEX_HOME="$tmp_env_root/codex" CLAUDE_HOME="$tmp_env_root/claude" \
   BEAM_INSTALL_BUNDLE_DIR="$tmp_bundle_dir" bash tests/test-beam-wrapper.sh > /dev/null
 
-echo "[broker-slow] install tests"
-bash tests/test-install.sh > /dev/null
-
 echo "[broker-slow] save replay tests"
 HOME="$tmp_env_root/home" CODEX_HOME="$tmp_env_root/codex" CLAUDE_HOME="$tmp_env_root/claude" \
   BEAM_INSTALL_BUNDLE_DIR="$tmp_bundle_dir" bash tests/test-broker-save-olean.sh > /dev/null
-
-ROCQ_LSP=""
-for candidate in "_opam/bin/coq-lsp" "_opam/_opam/bin/coq-lsp"; do
-  if [ -x "$candidate" ]; then
-    ROCQ_LSP="$candidate"
-    break
-  fi
-done
-
-if [ -n "$ROCQ_LSP" ]; then
-  echo "[broker-slow] rocq wrapper tests"
-  if [ -d "_opam/_opam" ]; then
-    eval "$(opam env --switch=./_opam --set-switch)"
-  fi
-  BEAM_ROCQ_CMD="$PWD/$ROCQ_LSP" bash tests/test-beam-wrapper-rocq.sh > /dev/null
-  echo "[broker-slow] rocq smoke test"
-  BEAM_ROCQ_CMD="$PWD/$ROCQ_LSP" .lake/build/bin/beam-daemon-rocq-smoke-test > /dev/null
-else
-  echo "[broker-slow] rocq skipped: install coq-lsp with tests/setup-rocq-opam.sh." >&2
-fi

tests/test-install.sh

@@ -58,7 +58,8 @@ export BEAM_INSTALL_ROOT="$tmp_root/install-root"
 
 mkdir -p "$HOME" "$BEAM_INSTALL_ROOT"
 
-toolchain="$(awk 'NR==1 {print $1}' lean-toolchain)"
+mapfile -t supported_toolchains < <(grep -v '^[[:space:]]*#' supported-lean-toolchains | sed '/^[[:space:]]*$/d')
+toolchain="${supported_toolchains[0]}"
 source_checkout="$tmp_root/source-checkout"
 
 assert_file() {
@@ -117,14 +118,14 @@ assert_runtime_layout() {
 assert_manifest_metadata() {
   local manifest_path="$1"
   local expected_payload="$2"
-  local expected_toolchain="$3"
-  local expected_source_commit="$4"
-  python3 - "$manifest_path" "$expected_payload" "$expected_toolchain" "$expected_source_commit" <<'PY'
+  local expected_source_commit="$3"
+  shift 3
+  python3 - "$manifest_path" "$expected_payload" "$expected_source_commit" "$@" <<'PY'
 import json
 import os
 import sys
 
-manifest_path, expected_payload, expected_toolchain, expected_source_commit = sys.argv[1:]
+manifest_path, expected_payload, expected_source_commit, *expected_toolchains = sys.argv[1:]
 with open(manifest_path, "r", encoding="utf-8") as f:
     manifest = json.load(f)
 layout = json.loads(os.environ["BEAM_INSTALL_LAYOUT_JSON"])
@@ -133,7 +134,7 @@ if manifest.get("schemaVersion") != 2:
     raise SystemExit(f"unexpected manifest schemaVersion: {manifest.get('schemaVersion')}")
 if manifest.get("payloadHash") != expected_payload:
     raise SystemExit(f"unexpected manifest payloadHash: {manifest.get('payloadHash')}")
-if manifest.get("toolchains") != [expected_toolchain]:
+if manifest.get("toolchains") != expected_toolchains:
     raise SystemExit(f"unexpected manifest toolchains: {manifest.get('toolchains')}")
 if "toolchain" in manifest:
     raise SystemExit(f"unexpected legacy manifest toolchain field: {manifest.get('toolchain')}")
@@ -206,25 +207,42 @@ path_without_elan() {
 
 assert_bundle_layout() {
   local bundle_root="$1"
-  local metadata
-  metadata="$(find "$bundle_root" -name metadata.json | head -n 1 || true)"
-  if [ -z "$metadata" ]; then
+  shift
+  local metadata_files=()
+  local metadata=""
+  local expected_toolchain=""
+  local found=""
+  mapfile -t metadata_files < <(find "$bundle_root" -name metadata.json | sort)
+  if [ "${#metadata_files[@]}" -eq 0 ]; then
     echo "missing bundle metadata under $bundle_root" >&2
     exit 1
   fi
-  if ! rg -n --fixed-strings "\"toolchain\": \"$toolchain\"" "$metadata" > /dev/null; then
-    echo "bundle metadata does not mention expected toolchain $toolchain: $metadata" >&2
-    exit 1
-  fi
-
-  local workspace
-  workspace="$(dirname "$metadata")/workspace"
-  assert_file "$workspace/Beam.lean"
-  assert_file "$workspace/Beam/Broker/Server.lean"
-  assert_file "$workspace/RunAt/Internal/SaveArtifacts.lean"
-  assert_file "$workspace/.lake/build/bin/beam-daemon"
-  assert_file "$workspace/.lake/build/bin/beam-client"
-  assert_file "$workspace/.lake/build/lib/librunAt_RunAt.so"
+  for expected_toolchain in "$@"; do
+    found=""
+    for metadata in "${metadata_files[@]}"; do
+      if command -v rg >/dev/null 2>&1; then
+        if rg -n --fixed-strings "\"toolchain\": \"$expected_toolchain\"" "$metadata" > /dev/null; then
+          found="$metadata"
+          break
+        fi
+      elif grep -F "\"toolchain\": \"$expected_toolchain\"" "$metadata" > /dev/null; then
+        found="$metadata"
+        break
+      fi
+    done
+    if [ -z "$found" ]; then
+      echo "bundle metadata does not mention expected toolchain $expected_toolchain under $bundle_root" >&2
+      exit 1
+    fi
+    local workspace
+    workspace="$(dirname "$found")/workspace"
+    assert_file "$workspace/Beam.lean"
+    assert_file "$workspace/Beam/Broker/Server.lean"
+    assert_file "$workspace/RunAt/Internal/SaveArtifacts.lean"
+    assert_file "$workspace/.lake/build/bin/beam-daemon"
+    assert_file "$workspace/.lake/build/bin/beam-client"
+    assert_file "$workspace/.lake/build/lib/librunAt_RunAt.so"
+  done
 }
 
 rsync -a --exclude='.git' ./ "$source_checkout"/
@@ -327,20 +345,20 @@ assert_version_count "$BEAM_INSTALL_ROOT/versions" 1
 installed_version_root="$(python3 -c 'import os,sys; print(os.path.realpath(sys.argv[1]))' "$installed_runtime_root")"
 installed_payload_id="$(basename "$installed_version_root")"
 assert_file "$installed_runtime_root/manifest.json"
-BEAM_INSTALL_LAYOUT_JSON="$install_layout_json" assert_manifest_metadata "$installed_runtime_root/manifest.json" "$installed_payload_id" "$toolchain" "$expected_source_commit"
+BEAM_INSTALL_LAYOUT_JSON="$install_layout_json" assert_manifest_metadata "$installed_runtime_root/manifest.json" "$installed_payload_id" "$expected_source_commit" "$toolchain"
 
 assert_not_exists "$CODEX_HOME"
 assert_not_exists "$CLAUDE_HOME"
-assert_bundle_layout "$BEAM_INSTALL_ROOT/state/install-bundles"
+assert_bundle_layout "$BEAM_INSTALL_ROOT/state/install-bundles" "$toolchain"
 
 (
   cd "$source_checkout"
   bash scripts/install-beam.sh --all-supported > /dev/null
 )
 
 assert_version_count "$BEAM_INSTALL_ROOT/versions" 1
-BEAM_INSTALL_LAYOUT_JSON="$install_layout_json" assert_manifest_metadata "$installed_runtime_root/manifest.json" "$installed_payload_id" "$toolchain" "$expected_source_commit"
-assert_bundle_layout "$BEAM_INSTALL_ROOT/state/install-bundles"
+BEAM_INSTALL_LAYOUT_JSON="$install_layout_json" assert_manifest_metadata "$installed_runtime_root/manifest.json" "$installed_payload_id" "$expected_source_commit" "$toolchain"
+assert_bundle_layout "$BEAM_INSTALL_ROOT/state/install-bundles" "${supported_toolchains[@]}"
 
 (
   cd "$source_checkout"
@@ -354,7 +372,7 @@ for skills_home in "$CODEX_HOME" "$CLAUDE_HOME"; do
   assert_no_skill_socket_guidance "$skills_home/skills/rocq-beam/SKILL.md"
 done
 assert_version_count "$BEAM_INSTALL_ROOT/versions" 1
-BEAM_INSTALL_LAYOUT_JSON="$install_layout_json" assert_manifest_metadata "$installed_runtime_root/manifest.json" "$installed_payload_id" "$toolchain" "$expected_source_commit"
+BEAM_INSTALL_LAYOUT_JSON="$install_layout_json" assert_manifest_metadata "$installed_runtime_root/manifest.json" "$installed_payload_id" "$expected_source_commit" "$toolchain"
 
 blocked_home="$tmp_root/blocked-home"
 blocked_install_root="$tmp_root/blocked-install-root"

tests/test-toolchain-compat.sh

@@ -0,0 +1,49 @@
+#!/usr/bin/env bash
+
+# Copyright (c) 2026 Lean FRO LLC. All rights reserved.
+# Released under Apache 2.0 license as described in the file LICENSE.
+# Author: Emilio J. Gallego Arias
+
+set -euo pipefail
+
+cd "$(dirname "$0")/.."
+
+toolchain="${1:-}"
+if [ -z "$toolchain" ]; then
+  echo "usage: bash tests/test-toolchain-compat.sh <toolchain>" >&2
+  exit 1
+fi
+
+tmp_bundle_dir="$(mktemp -d /tmp/beam-toolchain-bundles-XXXXXX)"
+tmp_env_root="$(mktemp -d /tmp/beam-toolchain-env-XXXXXX)"
+
+expect_owned_tmp_dir() {
+  case "$1" in
+    /tmp/beam-toolchain-bundles-*|/tmp/beam-toolchain-env-*)
+      ;;
+    *)
+      echo "refusing to touch unexpected temp dir: $1" >&2
+      exit 1
+      ;;
+  esac
+}
+
+cleanup() {
+  expect_owned_tmp_dir "$tmp_bundle_dir"
+  expect_owned_tmp_dir "$tmp_env_root"
+  rm -rf -- "$tmp_bundle_dir" "$tmp_env_root"
+}
+trap cleanup EXIT
+
+mkdir -p "$tmp_env_root/home" "$tmp_env_root/codex" "$tmp_env_root/claude"
+
+echo "[toolchain-compat] build"
+lake build beam-cli > /dev/null
+
+echo "[toolchain-compat] bundle install $toolchain"
+env -u BEAM_HOME -u BEAM_INSTALL_BUNDLE_DIR -u BEAM_CONTROL_DIR \
+  HOME="$tmp_env_root/home" \
+  CODEX_HOME="$tmp_env_root/codex" \
+  CLAUDE_HOME="$tmp_env_root/claude" \
+  BEAM_INSTALL_BUNDLE_DIR="$tmp_bundle_dir" \
+  ./.lake/build/bin/beam-cli bundle-install "$toolchain" > /dev/null