Skip to content

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

Merged
gauss-math-inc merged 2 commits into
mainfrom
codex/public-installer-lean-and-morph-20260330
Mar 30, 2026
Merged

fix(installer): stop forcing setup and expose Lean bootstrap errors#439
gauss-math-inc merged 2 commits into
mainfrom
codex/public-installer-lean-and-morph-20260330

Conversation

@gauss-math-inc

Copy link
Copy Markdown
Collaborator

Summary

  • stop forcing gauss setup from the generated launcher and keep installer auto mode non-interactive
  • surface elan/Lean bootstrap failures with captured output and recovery hints
  • extend the Ubuntu installer smoke to assert the new launcher behavior and readable bad-toolchain failures

Validation

  • bash -n scripts/install-internal.sh
  • bash -n tests/installer/ubuntu_repository_local_install_smoke/run-in-container.sh
  • invalid toolchain repro: GAUSS_LEAN_TOOLCHAIN=leanprover/lean4:v0.0.0-opengauss-public ./scripts/install-internal.sh ... exits with a clear error, captured elan output, and a recovery command
  • successful installer run against an existing Lean workspace with --skip-setup, including managed /prove staging verification and a launcher assertion that GAUSS_FORCE_FIRST_TIME_SETUP=1 gauss setup || true is absent
  • interactive no-key install in auto mode completes without prompting and ends with Skipping setup wizard prompt in auto mode; run \gauss setup` later...`
  • top-level ./scripts/install.sh run reaches the local template flow successfully and writes a launcher without the forced setup line

Notes

  • docker is not installed in this devbox, so I did not run the Docker wrapper around the Ubuntu smoke scenario here

@gauss-math-inc
gauss-math-inc merged commit 57ebaae into main Mar 30, 2026
1 check failed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant