Merge pull request #437 from math-inc/codex/public-managed-doctor-20260328

gauss-math-inc · web-flow · commit 45e5b6394beb · 2026-03-27T19:51:39.000-07:00
Add managed workflow checks to gauss doctor
diff --git a/README.md b/README.md
@@ -106,7 +106,7 @@ gauss update
 
 ```
 gauss                         # Launch the CLI
-/project create ~/my-project  # Create a new Lean project
+/project create ~/my-project --template-source <template-or-git-url>
 /prove 1+1=2                  # Spawn a proving agent
 /swarm                        # See running agents
 ```
@@ -138,6 +138,10 @@ Gauss treats Lean work as project-scoped by default. Before launching managed wo
 - `/project use [path]` pins the current session to an existing Gauss project
 - `/project clear` removes the session override and falls back to ambient project discovery
 
+If you use `/project create` often, set a default template once with
+`gauss.project.template_source` in `~/.gauss/config.yaml` or the
+`GAUSS_BLUEPRINT_TEMPLATE_SOURCE` environment variable.
+
 Gauss discovers `.gauss/project.yaml` upward from the current working directory, but managed workflow child agents launch from the active project root so the forwarded Lean workflow command always runs in the right project context.
 
 ## Workflow commands
@@ -169,6 +173,9 @@ Gauss discovers `.gauss/project.yaml` upward from the current working directory,
 - An active Gauss project selected via `.gauss/project.yaml`
 
 Gauss checks these before launch and tells you exactly what is missing.
+`gauss doctor` also reports the managed-workflow backend, auth mode, `uv` / `lake`
+availability, and whether the current working directory resolves to an active
+Gauss project.
 
 ---
 
diff --git a/gauss_cli/doctor.py b/gauss_cli/doctor.py
@@ -9,6 +9,7 @@
 import subprocess
 import shutil
 from pathlib import Path
+from typing import Any, Mapping
 
 from gauss_cli.branding import get_cli_command_name, get_product_name, rewrite_cli_references
 from gauss_cli.config import get_project_root, get_gauss_home, get_env_path
@@ -106,6 +107,189 @@ def _check_gateway_service_linger(issues: list[str]) -> None:
         check_warn("Could not verify systemd linger", f"({linger_detail})")
 
 
+def _check_managed_workflow_requirements(
+    issues: list[str],
+    *,
+    config: Mapping[str, Any] | None = None,
+    env: Mapping[str, str] | None = None,
+    active_cwd: str | Path | None = None,
+    cli_name: str | None = None,
+) -> None:
+    """Report Lean workflow prerequisites that are specific to Open Gauss."""
+    try:
+        from gauss_cli.autoformalize import (
+            CODEX_AUTOFORMALIZE_BACKEND,
+            DEFAULT_AUTOFORMALIZE_BACKEND,
+            _codex_auth_payload_has_api_key,
+            _codex_auth_payload_is_valid,
+            _has_local_claude_api_key,
+            _has_local_claude_login,
+            _load_local_codex_auth_payload,
+            _resolve_auth_mode,
+            _resolve_backend_name,
+            _resolve_claude_auth_env,
+            _resolve_codex_api_key,
+            _resolve_uv_runner,
+        )
+        from gauss_cli.project import (
+            ProjectManifestError,
+            ProjectNotFoundError,
+            discover_gauss_project,
+            resolve_template_source,
+        )
+    except Exception as exc:
+        print()
+        print(color("◆ Managed Lean Workflows", Colors.CYAN, Colors.BOLD))
+        check_warn("Managed workflow diagnostics unavailable", f"({exc})")
+        return
+
+    from gauss_cli.config import load_config
+
+    cli_name = cli_name or get_cli_command_name()
+    environment = dict(env or os.environ)
+    resolved_config = config if isinstance(config, Mapping) else load_config()
+
+    print()
+    print(color("◆ Managed Lean Workflows", Colors.CYAN, Colors.BOLD))
+
+    try:
+        backend_name = _resolve_backend_name(resolved_config, environment)
+        auth_mode = _resolve_auth_mode(resolved_config, environment)
+    except Exception as exc:
+        check_fail("Managed workflow config", f"({exc})")
+        issues.append(f"Fix gauss.autoformalize config: {exc}")
+        return
+
+    check_ok("Managed backend", f"({backend_name})")
+    check_ok("Managed auth mode", f"({auth_mode})")
+
+    template_source = resolve_template_source(resolved_config, environment)
+    if template_source:
+        check_ok("Project template source", f"({template_source})")
+    else:
+        check_warn(
+            "Project template source",
+            "(`/project create` needs `--template-source` or `gauss.project.template_source`)",
+        )
+
+    try:
+        uv_runner = _resolve_uv_runner(environment)
+        check_ok("uv / uvx", f"({Path(uv_runner[0]).name})")
+    except Exception as exc:
+        check_fail("uv / uvx", f"({exc})")
+        issues.append("Install uv so Gauss can launch the managed Lean MCP server")
+
+    lake_executable = shutil.which("lake", path=environment.get("PATH"))
+    if lake_executable:
+        check_ok("Lean toolchain (lake)", f"({lake_executable})")
+    else:
+        check_fail("Lean toolchain (lake)", "(required for managed Lean workflows)")
+        issues.append("Install elan / Lean so `lake` is available on PATH")
+
+    active_dir = Path(active_cwd or environment.get("TERMINAL_CWD") or os.getcwd()).expanduser().resolve()
+    if active_dir.exists():
+        check_ok("Active working directory", f"({active_dir})")
+        try:
+            project = discover_gauss_project(active_dir)
+            check_ok("Active Gauss project", f"({project.label})")
+        except ProjectNotFoundError:
+            check_warn("Active Gauss project", f"(none under {active_dir})")
+            issues.append(
+                "Create or select a Gauss project with `/project init`, `/project convert`, or `/project use <path>`"
+            )
+        except ProjectManifestError as exc:
+            check_fail("Gauss project manifest", f"({exc})")
+            issues.append(f"Repair the active Gauss project manifest: {exc}")
+    else:
+        check_fail("Active working directory", f"({active_dir} does not exist)")
+        issues.append(f"Fix the managed workflow working directory: {active_dir}")
+
+    real_home = Path(environment.get("HOME", str(Path.home()))).expanduser().resolve()
+
+    if backend_name == DEFAULT_AUTOFORMALIZE_BACKEND:
+        claude_executable = shutil.which("claude", path=environment.get("PATH"))
+        if claude_executable:
+            check_ok("Claude Code CLI", f"({claude_executable})")
+        else:
+            check_fail("Claude Code CLI", "(install with `npm install -g @anthropic-ai/claude-code`)")
+            issues.append("Install the Claude Code CLI for managed Lean workflows")
+
+        has_local_login = _has_local_claude_login(real_home)
+        has_local_api_key = _has_local_claude_api_key(real_home)
+        staged_auth_env = _resolve_claude_auth_env(environment, include_persisted_env=True)
+        staged_keys = ", ".join(sorted(staged_auth_env))
+
+        if auth_mode == "auto":
+            if has_local_login:
+                check_ok("Claude auth", "(local Claude login)")
+            elif has_local_api_key:
+                check_ok("Claude auth", "(local Claude API key)")
+            elif staged_auth_env:
+                check_ok("Claude auth", f"(staged via {staged_keys})")
+            else:
+                check_fail("Claude auth", "(not found)")
+                issues.append(
+                    "Run `claude auth login`, save `ANTHROPIC_API_KEY`, or set `gauss.autoformalize.auth_mode: login`"
+                )
+        elif auth_mode == "login":
+            if has_local_login:
+                check_ok("Claude auth", "(local Claude login)")
+            elif has_local_api_key:
+                check_warn("Claude auth", "(login mode ignores local Claude API keys; first launch will prompt)")
+            else:
+                check_warn("Claude auth", "(login mode will prompt on first launch)")
+        else:
+            if staged_auth_env:
+                check_ok("Claude API-key auth", f"(staged via {staged_keys})")
+            elif has_local_api_key:
+                check_ok("Claude API-key auth", "(local Claude API key)")
+            else:
+                check_fail("Claude API-key auth", "(not found)")
+                issues.append(
+                    "Save `ANTHROPIC_API_KEY` / `ANTHROPIC_TOKEN` / `CLAUDE_CODE_OAUTH_TOKEN`, or switch `gauss.autoformalize.auth_mode` back to `auto` or `login`"
+                )
+        return
+
+    if backend_name == CODEX_AUTOFORMALIZE_BACKEND:
+        codex_executable = shutil.which("codex", path=environment.get("PATH"))
+        if codex_executable:
+            check_ok("Codex CLI", f"({codex_executable})")
+        else:
+            check_fail("Codex CLI", "(install the OpenAI Codex CLI)")
+            issues.append("Install the OpenAI Codex CLI for managed Lean workflows")
+
+        local_auth_payload = _load_local_codex_auth_payload(real_home, environment)
+        has_local_auth = _codex_auth_payload_is_valid(local_auth_payload)
+        has_local_api_key = _codex_auth_payload_has_api_key(local_auth_payload)
+        staged_api_key = _resolve_codex_api_key(environment, include_persisted_env=True)
+
+        if auth_mode == "auto":
+            if has_local_auth:
+                check_ok("Codex auth", "(local Codex auth)")
+            elif staged_api_key:
+                check_ok("Codex auth", "(staged OPENAI_API_KEY)")
+            else:
+                check_fail("Codex auth", "(not found)")
+                issues.append(
+                    "Run `codex login`, save `OPENAI_API_KEY`, or set `gauss.autoformalize.auth_mode: login`"
+                )
+        elif auth_mode == "login":
+            if has_local_auth:
+                check_ok("Codex auth", "(local Codex auth)")
+            else:
+                check_warn("Codex auth", "(login mode will prompt on first launch)")
+        else:
+            if staged_api_key:
+                check_ok("Codex API-key auth", "(staged OPENAI_API_KEY)")
+            elif has_local_api_key:
+                check_ok("Codex API-key auth", "(local Codex API key)")
+            else:
+                check_fail("Codex API-key auth", "(not found)")
+                issues.append(
+                    "Save `OPENAI_API_KEY`, or switch `gauss.autoformalize.auth_mode` back to `auto` or `login`"
+                )
+
+
 def run_doctor(args):
     """Run diagnostic checks."""
     should_fix = getattr(args, 'fix', False)
@@ -485,6 +669,8 @@ def run_doctor(args):
             except Exception:
                 pass
 
+    _check_managed_workflow_requirements(issues, cli_name=cli_name)
+
     # =========================================================================
     # Check: API connectivity
     # =========================================================================
diff --git a/tests/gauss_cli/test_doctor.py b/tests/gauss_cli/test_doctor.py
@@ -1,16 +1,20 @@
 """Tests for gauss_cli.doctor."""
 
+import json
 import os
 import sys
 import types
 from argparse import Namespace
+from pathlib import Path
 
 import pytest
 
+import gauss_cli.autoformalize as autoformalize_mod
 import gauss_cli.doctor as doctor
 import gauss_cli.gateway as gateway_cli
 from gauss_cli import doctor as doctor_mod
 from gauss_cli.doctor import _has_provider_env_config
+from gauss_cli.project import initialize_gauss_project
 
 
 class TestProviderEnvDetection:
@@ -101,3 +105,120 @@ def test_check_gateway_service_linger_skips_when_service_not_installed(monkeypat
     out = capsys.readouterr().out
     assert out == ""
     assert issues == []
+
+
+def _write_executable(path: Path) -> None:
+    path.write_text("#!/usr/bin/env bash\nexit 0\n", encoding="utf-8")
+    path.chmod(0o755)
+
+
+def test_check_managed_workflow_requirements_reports_healthy_claude_setup(tmp_path, capsys):
+    bin_dir = tmp_path / "bin"
+    home_dir = tmp_path / "home"
+    project_root = tmp_path / "project"
+    bin_dir.mkdir()
+    (home_dir / ".claude").mkdir(parents=True)
+    for name in ("claude", "uvx", "lake"):
+        _write_executable(bin_dir / name)
+
+    (home_dir / ".claude" / ".credentials.json").write_text(
+        json.dumps({"claudeAiOauth": {"accessToken": "token"}}),
+        encoding="utf-8",
+    )
+    project_root.mkdir()
+    (project_root / "lakefile.lean").write_text("-- lean project\n", encoding="utf-8")
+    initialize_gauss_project(project_root, name="Demo Project")
+
+    issues: list[str] = []
+    doctor._check_managed_workflow_requirements(
+        issues,
+        config={
+            "gauss": {
+                "autoformalize": {"backend": "claude-code", "auth_mode": "auto"},
+                "project": {"template_source": "https://example.com/template.git"},
+            }
+        },
+        env={"PATH": str(bin_dir), "HOME": str(home_dir)},
+        active_cwd=project_root,
+        cli_name="gauss",
+    )
+
+    output = capsys.readouterr().out
+    assert "Managed Lean Workflows" in output
+    assert "Managed backend" in output
+    assert "claude-code" in output
+    assert "Active Gauss project" in output
+    assert "Demo Project" in output
+    assert "Claude auth" in output
+    assert "local Claude login" in output
+    assert issues == []
+
+
+def test_check_managed_workflow_requirements_reports_missing_codex_prereqs(monkeypatch, tmp_path, capsys):
+    missing_project_dir = tmp_path / "outside"
+    home_dir = tmp_path / "home"
+    missing_project_dir.mkdir()
+    home_dir.mkdir()
+    monkeypatch.setattr(autoformalize_mod, "get_env_value", lambda _key: None)
+
+    issues: list[str] = []
+    doctor._check_managed_workflow_requirements(
+        issues,
+        config={
+            "gauss": {
+                "autoformalize": {"backend": "codex", "auth_mode": "api-key"},
+            }
+        },
+        env={"PATH": "", "HOME": str(home_dir)},
+        active_cwd=missing_project_dir,
+        cli_name="gauss",
+    )
+
+    output = capsys.readouterr().out
+    assert "Codex CLI" in output
+    assert "Codex API-key auth" in output
+    assert "Active Gauss project" in output
+    assert "uv / uvx" in output
+    assert "Lean toolchain (lake)" in output
+    assert any("Codex CLI" in issue or "OpenAI Codex CLI" in issue for issue in issues)
+    assert any("OPENAI_API_KEY" in issue for issue in issues)
+    assert any("/project init" in issue for issue in issues)
+    assert any("uv" in issue for issue in issues)
+    assert any("lake" in issue for issue in issues)
+
+
+def test_check_managed_workflow_requirements_warns_when_claude_login_mode_only_has_api_key(tmp_path, capsys):
+    bin_dir = tmp_path / "bin"
+    home_dir = tmp_path / "home"
+    project_root = tmp_path / "project"
+    bin_dir.mkdir()
+    (home_dir / ".claude").mkdir(parents=True)
+    for name in ("claude", "uvx", "lake"):
+        _write_executable(bin_dir / name)
+
+    (home_dir / ".claude.json").write_text(
+        json.dumps({"primaryApiKey": "sk-ant-api-key"}),
+        encoding="utf-8",
+    )
+    project_root.mkdir()
+    (project_root / "lakefile.lean").write_text("-- lean project\n", encoding="utf-8")
+    initialize_gauss_project(project_root, name="Login Mode Project")
+
+    issues: list[str] = []
+    doctor._check_managed_workflow_requirements(
+        issues,
+        config={
+            "gauss": {
+                "autoformalize": {"backend": "claude-code", "auth_mode": "login"},
+                "project": {"template_source": "https://example.com/template.git"},
+            }
+        },
+        env={"PATH": str(bin_dir), "HOME": str(home_dir)},
+        active_cwd=project_root,
+        cli_name="gauss",
+    )
+
+    output = capsys.readouterr().out
+    assert "Claude auth" in output
+    assert "login mode ignores local Claude API keys" in output
+    assert issues == []
