test(installer): add tiny managed /prove staging smoke

tests/installer/README.md

@@ -20,3 +20,15 @@ Current scenarios:
   - verifies the installer bootstraps its own Debian/Ubuntu prerequisites
   - stages a dummy `OPENAI_API_KEY` to test non-interactive provider setup
   - verifies the workflow-derived workspace, config, guide, and helper scripts
+
+- `ubuntu_managed_prove_sorry_smoke`
+  Verifies that a stock `ubuntu:24.04` container can install from the current
+  checkout and stage a managed `/prove` run against a tiny Lean project
+  containing one `sorry`. This scenario:
+  - installs via `./scripts/install-internal.sh` from a mounted git checkout
+  - accepts either `ANTHROPIC_API_KEY` (Claude backend) or `OPENAI_API_KEY`
+    (Codex backend)
+  - initializes a local `.gauss` manifest in the fixture project
+  - verifies the staged startup context, managed skill, and backend instructions
+  - verifies the managed MCP config points `LEAN_PROJECT_PATH` at the fixture
+  - leaves an opt-in `LIVE_MANAGED_PROVE_SMOKE=1` path for manual backend runs

tests/installer/fixtures/lean_hello_sorry/HelloSorry.lean

@@ -0,0 +1 @@
+import HelloSorry.Basic

tests/installer/fixtures/lean_hello_sorry/HelloSorry/Basic.lean

@@ -0,0 +1,6 @@
+namespace HelloSorry
+
+theorem hello_world : True := by
+  sorry
+
+end HelloSorry

tests/installer/fixtures/lean_hello_sorry/lakefile.toml

@@ -0,0 +1,6 @@
+name = "HelloSorry"
+version = "0.1.0"
+defaultTargets = ["HelloSorry"]
+
+[[lean_lib]]
+name = "HelloSorry"

tests/installer/fixtures/lean_hello_sorry/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.28.0

tests/installer/ubuntu_managed_prove_sorry_smoke/Dockerfile

@@ -0,0 +1,5 @@
+FROM ubuntu:24.04
+
+SHELL ["/bin/bash", "-lc"]
+
+CMD ["/bin/bash"]

tests/installer/ubuntu_managed_prove_sorry_smoke/README.md

@@ -0,0 +1,33 @@
+# Ubuntu Managed `/prove` Staging Smoke
+
+This scenario verifies that a clean `ubuntu:24.04` container can:
+
+1. install Open Gauss from the current checkout with `./scripts/install-internal.sh`
+2. copy a tiny Lean project that contains one `sorry`
+3. initialize a local `.gauss` manifest in that project
+4. stage a managed `/prove HelloSorry/Basic.lean` launch against that project
+5. confirm the staged skill, startup context, backend instructions, and MCP
+   config all point at the tiny Lean project correctly
+
+Provider requirements:
+
+- set `ANTHROPIC_API_KEY` to exercise the Claude-managed backend, or
+- set `OPENAI_API_KEY` to exercise the Codex-managed backend
+
+Usage:
+
+```bash
+tests/installer/ubuntu_managed_prove_sorry_smoke/run.sh
+```
+
+Notes:
+
+- The scenario mounts the current checkout at `/src`, so it always exercises
+  the branch you are testing without needing GitHub access inside the container.
+- The default path is deterministic: it validates managed staging only, not a
+  full model-driven proof attempt.
+- Set `LIVE_MANAGED_PROVE_SMOKE=1` to turn on the best-effort live backend
+  execution path for manual debugging. That path is intentionally not the
+  default smoke because backend/model timing can make it flaky.
+- The fixture intentionally stays tiny so the smoke focuses on managed proving,
+  not on a large project setup.