Skip to content

Trim provider clutter from Morph onboarding #445

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
gauss-math-inc merged 1 commit into from
Apr 2, 2026
Merged

Trim provider clutter from Morph onboarding #445

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
60 changes: 15 additions & 45 deletions scripts/install-internal.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1166,12 +1166,12 @@ guide_html = f"""<!DOCTYPE html>
<p>Commit important changes, push to a remote, and use any save or snapshot feature Morph exposes before closing the tab. Avoid leaving important work only in temp directories.</p>
</div>
<div class="card">
<strong>Ready Paths</strong>
<p><code>{escape(str(repo_root))}</code><br><code>{escape(str(workspace_dir))}</code><br><code>{escape(str(gauss_home / ".env"))}</code><br><code>{escape(str(start_here_doc))}</code></p>
<strong>Open Gauss Prepared</strong>
<p><code>{escape(str(repo_root))}</code><br><code>{escape(str(workspace_dir))}</code><br><code>{escape(str(start_here_doc))}</code></p>
</div>
<div class="card">
<strong>Backend Helpers</strong>
<p><code>gauss-use-claude-backend</code><br><code>gauss-use-codex-backend</code><br><code>gauss-use-auto-auth</code><br><code>gauss-use-claude-login</code><br><code>gauss-use-codex-login</code></p>
<strong>Change Settings Later</strong>
<p>Run <code>gauss setup</code> if you want to review providers, switch models, or change other defaults after the first session.</p>
</div>
</section>
<main>
Expand Down Expand Up @@ -1467,22 +1467,15 @@ if [ "${1:-}" = "--print-summary" ]; then
shift
fi

staged_keys="none"
if [ -n "${OPENROUTER_API_KEY:-}" ] || [ -n "${OPENAI_API_KEY:-}" ] || [ -n "${ANTHROPIC_API_KEY:-}" ]; then
staged_keys=""
[ -n "${OPENROUTER_API_KEY:-}" ] && staged_keys="${staged_keys} OPENROUTER_API_KEY"
[ -n "${OPENAI_API_KEY:-}" ] && staged_keys="${staged_keys} OPENAI_API_KEY"
[ -n "${ANTHROPIC_API_KEY:-}" ] && staged_keys="${staged_keys} ANTHROPIC_API_KEY"
staged_keys="${staged_keys# }"
fi

interactive_provider="none staged"
main_chat_status="needs setup."
launcher_behavior="Because no main chat provider is staged, this launcher will run gauss setup first and then leave you in a shell."
launch_gauss=0
if provider_status="$(gauss-configure-main-provider auto 2>&1)"; then
interactive_provider="$provider_status"
main_chat_status="ready."
launcher_behavior="This launcher opens Gauss automatically and begins with /start."
launch_gauss=1
else
interactive_provider="$provider_status"
:
fi

clear >/dev/null 2>&1 || true
Expand All @@ -1495,10 +1488,8 @@ Commit: $(git -C "$REPO_ROOT" rev-parse --short=12 HEAD 2>/dev/null || printf 'u
Lean project: $WORKSPACE_DIR
Guide: __GUIDE_PATH__
Gauss project manifest: initialized
Default managed backend: claude-code
Default auth mode: auto
Main interactive provider: ${interactive_provider}
Staged keys: ${staged_keys}
Managed backend: claude-code
Main chat: ${main_chat_status}

Start here:
gauss-open-guide
Expand All @@ -1518,24 +1509,11 @@ Lean workflows:
/autoformalize --source ./paper.pdf --claim-select=first --out=Paper.lean
/swarm

Backend helpers:
gauss-use-claude-backend
gauss-use-codex-backend
gauss-use-auto-auth
gauss-use-claude-login
gauss-use-codex-login
gauss-use-openrouter-key
gauss-use-anthropic-key
gauss-use-openai-key

Interactive provider notes:
Auto-selection priority: OpenRouter, then Anthropic, then OpenAI-compatible.
OpenRouter affects the in-process main chat only; managed workflow backends stay separate.
Notes:
/start keeps you in Gauss and enables inline onboarding chat before project selection.
/chat opens the configured managed backend chat session and returns you to Gauss when it exits.
gauss-use-claude-backend and gauss-use-codex-backend switch both /chat and the managed Lean workflows.
When the main provider is staged, this launcher opens Gauss automatically and begins with /start.
If no main provider is staged, this launcher runs gauss setup first and then falls back to a shell.
Run gauss setup later if you want to review or change providers and other settings.
$launcher_behavior
PROMPT_TOOLKIT_NO_CPR=1 is enabled to avoid CPR warnings inside tmux.

The local guide is written to __GUIDE_PATH__.
Expand Down Expand Up @@ -1745,15 +1723,6 @@ print_summary() {
echo
echo " Inside Gauss, use /prove, /review, /draft, /autoprove, /formalize, or /autoformalize once a project is active."
echo
printf '%b%s%b\n' "${CYAN}${BOLD}" "Helper Commands:" "${NC}"
echo " gauss-configure-main-provider [auto|openrouter|anthropic|openai]"
echo " gauss-use-openrouter-key"
echo " gauss-use-anthropic-key"
echo " gauss-use-openai-key"
echo " gauss-use-claude-backend"
echo " gauss-use-codex-backend"
echo " gauss-use-auto-auth"
echo
printf '%b%s%b\n' "${CYAN}${BOLD}" "Notes:" "${NC}"
echo " - The installer keeps code in your existing repository checkout."
echo " - The installer updates future shells, but it cannot change PATH in the shell that launched the installer."
Expand All @@ -1766,6 +1735,7 @@ print_summary() {
fi
echo " - The local guide is written to $GUIDE_DIR/index.html."
echo " - If Open Gauss feels intimidating, start with /start for inline onboarding or /chat for managed backend chat."
echo " - Use gauss setup later if you want to review providers or other settings."
echo " - No Morph iframe is exposed automatically; use gauss-open-guide if you want the local guide in a browser."
echo " - No tmux session is opened during install; use gauss-open-session when you want the workflow launcher."
}
Expand Down
28 changes: 25 additions & 3 deletions tests/installer/ubuntu_repository_local_install_smoke/run-in-container.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -57,6 +57,12 @@ grep -F "/start" "$INSTALL_LOG" >/dev/null || die "expected installer summary to
grep -F "gauss-open-session" "$INSTALL_LOG" >/dev/null || die "expected installer summary to mention gauss-open-session"
grep -F "gauss-open-guide" "$INSTALL_LOG" >/dev/null || die "expected installer summary to mention gauss-open-guide"
grep -F "cannot change PATH in the shell that launched the installer." "$INSTALL_LOG" >/dev/null || die "expected installer summary to explain current-shell PATH behavior"
if grep -F "Helper Commands:" "$INSTALL_LOG" >/dev/null; then
die "expected installer summary to avoid helper-command clutter"
fi
if grep -F "gauss-use-openrouter-key" "$INSTALL_LOG" >/dev/null; then
die "expected installer summary to avoid provider-key helper clutter"
fi
grep -F "Managed Lean workflow assets ready:" "$INSTALL_LOG" >/dev/null || die "expected installer to prewarm managed Lean workflow assets"
grep -F "Managed /prove staging verified:" "$INSTALL_LOG" >/dev/null || die "expected installer to verify managed /prove staging in the Lean workspace"
if grep -F "Skipping managed /prove staging verification" "$INSTALL_LOG" >/dev/null; then
Expand Down Expand Up @@ -87,6 +93,12 @@ grep -F "Start Here" "$GAUSS_HOME/guide/index.html" >/dev/null || die "expected
grep -F "/start" "$GAUSS_HOME/guide/index.html" >/dev/null || die "expected generated guide to mention /start"
grep -F "/chat" "$GAUSS_HOME/guide/index.html" >/dev/null || die "expected generated guide to mention /chat"
grep -F "If You Opened This In Morph" "$GAUSS_HOME/guide/index.html" >/dev/null || die "expected generated guide to include Morph guidance"
if grep -F "gauss-use-claude-login" "$GAUSS_HOME/guide/index.html" >/dev/null; then
die "expected generated guide to avoid login-helper clutter"
fi
if grep -F "$GAUSS_HOME/.env" "$GAUSS_HOME/guide/index.html" >/dev/null; then
die "expected generated guide to avoid exposing the staged .env path"
fi
assert_exists "$GAUSS_HOME/autoformalize/assets/lean4-skills/.gauss-managed-revision"
assert_exists "$GAUSS_HOME/skins/mathinc.yaml"
assert_exists "$WORKSPACE_DIR/PAPER.md"
Expand Down Expand Up @@ -172,11 +184,21 @@ grep -F 'OPENAI_BASE_URL="https://api.openai.com/v1"' "$GAUSS_HOME/.env" >/dev/n
echo "==> Verifying launcher summary"
SUMMARY_OUTPUT="$(gauss-launch-session --print-summary)"
printf '%s\n' "$SUMMARY_OUTPUT"
[[ "$SUMMARY_OUTPUT" == *"OpenAI-compatible main provider configured"* ]] || die "expected OpenAI provider summary"
[[ "$SUMMARY_OUTPUT" == *"Managed backend: claude-code"* ]] || die "expected managed backend summary"
[[ "$SUMMARY_OUTPUT" == *"Main chat: ready."* ]] || die "expected ready main-chat summary"
[[ "$SUMMARY_OUTPUT" == *"$WORKSPACE_DIR"* ]] || die "expected workspace path in launcher summary"
[[ "$SUMMARY_OUTPUT" == *"/chat"* ]] || die "expected launcher summary to mention /chat"
[[ "$SUMMARY_OUTPUT" == *"gauss-open-guide"* ]] || die "expected launcher summary to mention gauss-open-guide"
[[ "$SUMMARY_OUTPUT" == *"begins with /start"* ]] || die "expected launcher summary to mention automatic /start"
if [[ "$SUMMARY_OUTPUT" == *"Staged keys:"* ]]; then
die "expected launcher summary to avoid staged-key details"
fi
if [[ "$SUMMARY_OUTPUT" == *"Gauss Setup — Non-interactive mode"* ]]; then
die "expected launcher summary to avoid inlined setup output"
fi
if [[ "$SUMMARY_OUTPUT" == *"gauss-use-openrouter-key"* ]]; then
die "expected launcher summary to avoid provider-key helper clutter"
fi

echo "==> Verifying no-provider launcher fallback state"
cp "$GAUSS_HOME/.env" "$GAUSS_HOME/.env.backup"
Expand All @@ -202,9 +224,9 @@ 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"
[[ "$NO_PROVIDER_SUMMARY" == *"Main chat: needs setup."* ]] || die "expected missing-provider launcher summary"
[[ "$NO_PROVIDER_SUMMARY" == *"/chat opens the configured managed backend chat session"* ]] || die "expected provider notes to mention managed /chat"
[[ "$NO_PROVIDER_SUMMARY" == *"runs gauss setup first"* ]] || die "expected missing-provider summary to mention setup fallback"
[[ "$NO_PROVIDER_SUMMARY" == *"run gauss setup first and then leave you in a shell"* ]] || die "expected missing-provider summary to mention setup fallback"
grep -F "GAUSS_FORCE_FIRST_TIME_SETUP=1 gauss setup || true" "$HOME/.local/bin/gauss-launch-session" >/dev/null || die "expected launcher to restore first-run setup fallback when no provider is staged"
grep -F "gauss --startup-input /start" "$HOME/.local/bin/gauss-launch-session" >/dev/null || die "expected launcher to auto-start gauss with /start"
grep -F "exec bash -i" "$HOME/.local/bin/gauss-launch-session" >/dev/null || die "expected interactive shell fallback when no provider is staged"
Expand Down
Loading