From 2e983e833e6c06f73c8bf77b9b57809ab140867a Mon Sep 17 00:00:00 2001 From: gauss-math-inc Date: Mon, 30 Mar 2026 16:09:48 +0000 Subject: [PATCH 1/2] fix(installer): stop forcing setup and expose lean errors --- scripts/install-internal.sh | 79 ++++++++++++++++--- .../run-in-container.sh | 24 +++++- 2 files changed, 88 insertions(+), 15 deletions(-) diff --git a/scripts/install-internal.sh b/scripts/install-internal.sh index bc16391..17da882 100755 --- a/scripts/install-internal.sh +++ b/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 | 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 "$@" diff --git a/tests/installer/ubuntu_repository_local_install_smoke/run-in-container.sh b/tests/installer/ubuntu_repository_local_install_smoke/run-in-container.sh index 63ec9ff..7fb8044 100755 --- a/tests/installer/ubuntu_repository_local_install_smoke/run-in-container.sh +++ b/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" From 7a7808af7d53e768a93370b8bfd3d91d8ca8d531 Mon Sep 17 00:00:00 2001 From: gauss-math-inc Date: Mon, 30 Mar 2026 16:23:13 +0000 Subject: [PATCH 2/2] fix(installer): make Lean toolchain detection robust --- scripts/install-internal.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/install-internal.sh b/scripts/install-internal.sh index 17da882..3394750 100755 --- a/scripts/install-internal.sh +++ b/scripts/install-internal.sh @@ -675,7 +675,7 @@ ensure_lean_toolchain() { exit 1 fi - if elan toolchain list 2>/dev/null | grep -Fx "$LEAN_TOOLCHAIN" >/dev/null 2>&1; then + 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 \