fix(installer): stop forcing setup and expose Lean bootstrap errors

scripts/install-internal.sh

@@ -205,6 +205,40 @@ log_error() {
     printf '%b%s%b %s\n' "${RED}" "${ERROR_MARK}" "${NC}" "$1"
 }
 
+print_captured_output() {
+    local output_file="$1"
+    if ! [ -s "$output_file" ]; then
+        return
+    fi
+    printf '%s\n' "Captured command output:"
+    sed 's/^/  /' "$output_file"
+}
+
+run_command_with_diagnostics() {
+    local error_message="$1"
+    local recovery_hint="$2"
+    shift 2
+
+    local output_file
+    local status
+    output_file="$(mktemp /tmp/opengauss-command.XXXXXX.log)"
+
+    "$@" >"$output_file" 2>&1
+    status=$?
+    if [ "$status" -eq 0 ]; then
+        rm -f "$output_file"
+        return 0
+    fi
+    log_error "$error_message"
+    print_captured_output "$output_file"
+    rm -f "$output_file"
+
+    if [ -n "$recovery_hint" ]; then
+        log_info "$recovery_hint"
+    fi
+    return "$status"
+}
+
 refresh_paths() {
     VENV_DIR="$REPO_ROOT/venv"
     VENV_BIN="$VENV_DIR/bin"
@@ -617,8 +651,21 @@ ensure_lean_toolchain() {
     if ! command -v elan >/dev/null 2>&1 && [ ! -x "$HOME/.elan/bin/elan" ]; then
         local elan_script
         elan_script="$(mktemp /tmp/elan-init.XXXXXX.sh)"
-        curl -L https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -o "$elan_script"
-        bash "$elan_script" -y
+        if ! run_command_with_diagnostics \
+            "Failed to download the elan installer." \
+            "Try: curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -o /tmp/elan-init.sh && bash /tmp/elan-init.sh -y" \
+            curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -o "$elan_script"; then
+            rm -f "$elan_script"
+            exit 1
+        fi
+        if ! run_command_with_diagnostics \
+            "Failed to install elan." \
+            "Try: bash /tmp/elan-init.sh -y && export PATH=\"\$HOME/.elan/bin:\$PATH\" && elan --version" \
+            bash "$elan_script" -y; then
+            rm -f "$elan_script"
+            exit 1
+        fi
+        rm -f "$elan_script"
     fi
 
     export PATH="$HOME/.elan/bin:$PATH"
@@ -628,8 +675,22 @@ ensure_lean_toolchain() {
         exit 1
     fi
 
-    elan toolchain install "$LEAN_TOOLCHAIN" >/dev/null 2>&1 || true
-    elan default "$LEAN_TOOLCHAIN" >/dev/null 2>&1
+    if elan toolchain list 2>/dev/null | awk '{print $1}' | grep -Fx "$LEAN_TOOLCHAIN" >/dev/null 2>&1; then
+        log_info "Lean toolchain $LEAN_TOOLCHAIN is already installed."
+    else
+        if ! run_command_with_diagnostics \
+            "Failed to install Lean toolchain $LEAN_TOOLCHAIN." \
+            "Try: export PATH=\"\$HOME/.elan/bin:\$PATH\" && elan toolchain install \"$LEAN_TOOLCHAIN\" && elan default \"$LEAN_TOOLCHAIN\" && lake --version" \
+            elan toolchain install "$LEAN_TOOLCHAIN"; then
+            exit 1
+        fi
+    fi
+    if ! run_command_with_diagnostics \
+        "Failed to select Lean toolchain $LEAN_TOOLCHAIN as the default." \
+        "Try: export PATH=\"\$HOME/.elan/bin:\$PATH\" && elan default \"$LEAN_TOOLCHAIN\" && lake --version" \
+        elan default "$LEAN_TOOLCHAIN"; then
+        exit 1
+    fi
 
     if ! command -v lake >/dev/null 2>&1; then
         log_error "lake is not available after configuring Lean."
@@ -1350,7 +1411,6 @@ fi
 
 cd "$WORKSPACE_DIR"
 if [ -t 0 ] && [ -t 1 ]; then
-  GAUSS_FORCE_FIRST_TIME_SETUP=1 gauss setup || true
   exec bash -i
 fi
 if [ "$launch_gauss" -eq 1 ]; then
@@ -1621,14 +1681,7 @@ run_setup_wizard() {
         log_info "Skipping setup wizard prompt because the main provider was auto-configured. Run \`gauss setup\` any time to review or change it."
         return
     fi
-
-    echo
-    read -p "Would you like to run the setup wizard now? (configure API keys + model) [Y/n] " -n 1 -r
-    echo
-    if [[ $REPLY =~ ^[Yy]$ ]] || [[ -z $REPLY ]]; then
-        echo
-        "$VENV_PYTHON" -m gauss_cli.main setup
-    fi
+    log_info "Skipping setup wizard prompt in auto mode; run 'gauss setup' later to configure keys or models."
 }
 
 main "$@"

tests/installer/ubuntu_repository_local_install_smoke/run-in-container.sh

@@ -62,7 +62,7 @@ if grep -F "Skipping managed /prove staging verification" "$INSTALL_LOG" >/dev/n
     die "expected installer managed /prove verification to run in the Lean workspace"
 fi
 if grep -F "Would you like to run the setup wizard now?" "$INSTALL_LOG" >/dev/null; then
-    die "expected installer to skip the setup wizard prompt when a main provider was auto-configured"
+    die "expected installer auto mode to stay non-interactive"
 fi
 if [ "$PATH_HAS_LOCAL_BIN" -ne 1 ] && command -v gauss >/dev/null 2>&1; then
     die "expected gauss to stay off PATH until the shell is reloaded"
@@ -194,8 +194,28 @@ PY
 NO_PROVIDER_SUMMARY="$(gauss-launch-session --print-summary)"
 printf '%s\n' "$NO_PROVIDER_SUMMARY"
 [[ "$NO_PROVIDER_SUMMARY" == *"No staged OpenRouter, Anthropic, or OpenAI key found for the main interactive provider."* ]] || die "expected missing-provider summary"
-grep -F "GAUSS_FORCE_FIRST_TIME_SETUP=1 gauss setup || true" "$HOME/.local/bin/gauss-launch-session" >/dev/null || die "expected forced first-time setup handoff in launcher"
+if grep -F "GAUSS_FORCE_FIRST_TIME_SETUP=1 gauss setup || true" "$HOME/.local/bin/gauss-launch-session" >/dev/null; then
+    die "expected launcher to stop forcing gauss setup"
+fi
 grep -F "exec bash -i" "$HOME/.local/bin/gauss-launch-session" >/dev/null || die "expected interactive shell fallback in launcher"
 mv "$GAUSS_HOME/.env.backup" "$GAUSS_HOME/.env"
 
+echo "==> Verifying Lean bootstrap failures surface useful diagnostics"
+BAD_TOOLCHAIN_HOME="/tmp/gauss-home-bad-toolchain"
+BAD_TOOLCHAIN_LOG="/tmp/opengauss-bad-toolchain.log"
+BAD_TOOLCHAIN_VALUE="leanprover/lean4:v0.0.0-opengauss-smoke"
+rm -rf "$BAD_TOOLCHAIN_HOME" "$BAD_TOOLCHAIN_LOG"
+if GAUSS_LEAN_TOOLCHAIN="$BAD_TOOLCHAIN_VALUE" ./scripts/install-internal.sh \
+    --gauss-home "$BAD_TOOLCHAIN_HOME" \
+    --workspace-dir /tmp/gauss-workspace-bad-toolchain \
+    --skip-system-packages \
+    --skip-setup \
+    >"$BAD_TOOLCHAIN_LOG" 2>&1; then
+    cat "$BAD_TOOLCHAIN_LOG"
+    die "expected invalid Lean toolchain bootstrap to fail"
+fi
+grep -F "Failed to install Lean toolchain $BAD_TOOLCHAIN_VALUE." "$BAD_TOOLCHAIN_LOG" >/dev/null || die "expected Lean toolchain failure message"
+grep -F "Captured command output:" "$BAD_TOOLCHAIN_LOG" >/dev/null || die "expected captured elan output"
+grep -F "Try: export PATH=\"\$HOME/.elan/bin:\$PATH\" && elan toolchain install \"$BAD_TOOLCHAIN_VALUE\"" "$BAD_TOOLCHAIN_LOG" >/dev/null || die "expected manual recovery hint"
+
 echo "==> ubuntu_repository_local_install_smoke passed"