diff --git a/AGENTS.md b/AGENTS.md index d81946e..04b1f72 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -19,8 +19,9 @@ Core rules: - Formalization/proof readiness should inspect local Lean readiness first; inspect Numina/backend readiness only when the user asks for an optional Lean-specialist backend. - Setup-only readiness should focus on local Lean/mathlib state, and should mention or inspect Numina only when the user asks for the optional official backend. - Do not require API keys for the default coding-agent path. -- Shared workspace is the default Lean project context; Numina may target it instead of upstream examples. -- Prefer the user's existing Lake project. Use the shared `${AI4MATH_HOME:-~/.ai4math}/lean-workspace` only when a standalone file needs project context. +- Shared workspace is the default Lean project context for standalone work; Numina may target it instead of upstream examples. +- Prefer the user's existing Lake project. Use the shared `${AI4MATH_HOME:-~/.ai4math}/lean-workspace` only when a standalone file needs project context, and default that managed workspace to `leanprover/lean4:v4.28.0` unless the user explicitly overrides it. +- Use `${AI4MATH_HOME:-~/.ai4math}/lean-workspaces//` for standalone tasks that need a different Lean/mathlib revision; do not overwrite the canonical managed workspace for version drift. - Preserve theorem statements unless the user explicitly approves a change. - Reject final patches containing `sorry`, `admit`, or newly introduced `axiom`. - Do not commit API keys, local runtime state, or machine-specific Numina paths. diff --git a/README.md b/README.md index ca691e0..c1046f1 100644 --- a/README.md +++ b/README.md @@ -66,6 +66,20 @@ For formalization or proof repair, start with: skills/lean-formalization/SKILL.md ``` +## Supported Scope + +- Lean project/workspace inspection. +- Reusable shared `~/.ai4math/lean-workspace` setup for standalone Lean files, using the AI4Math managed baseline `leanprover/lean4:v4.28.0` unless explicitly overridden. +- Theorem formalization, proof repair, proof completion, and `sorry` completion. +- Patch review for `sorry`, `admit`, newly introduced `axiom`, and theorem statement drift. +- Minimal failing Lean fragment extraction when a proof is blocked. +- Related-work-informed Lean-specialist patterns: theorem-state loops, premise retrieval, bounded proof search, failure memory, validation oracles, and minimal handoff. +- Optional Lean-specialist backend adapter flow, currently implemented for official `project-numina/numina-lean-agent` deployment/calls mediated by the coding agent. + +Numina is optional and is the only built-in deployable backend adapter. The public CLI does not expose a parallel `numina-*` workflow; `doctor` reports readiness and `configure --setup-numina --project-name ` performs the reviewed local setup under `~/.ai4math/numina-runtime/` by default. + +Future backend adapters can follow `skills/lean-runtime/references/backend_adapter_checklist.md`, but should not be described as supported until deployment, readiness checks, invocation, validation, and failure triage are documented. + ## Repository Layout ```text diff --git a/README.zh-CN.md b/README.zh-CN.md index e648d1d..87f3234 100644 --- a/README.zh-CN.md +++ b/README.zh-CN.md @@ -52,6 +52,23 @@ skills/lean-setup/SKILL.md skills/lean-formalization/SKILL.md ``` +`approve` 表示执行下一步，`revise` 表示先修改计划，`reject` 表示停止当前路线， +`skip` 表示跳过当前阶段。修改 theorem statement、设置 Numina、编辑源码和接受最终 proof +claim 前都应先请求用户确认。 + +## 支持范围 + +- Lean project/workspace inspection。 +- 只配置环境时，可创建或复用共享 `~/.ai4math/lean-workspace`；默认使用 AI4Math managed baseline `leanprover/lean4:v4.28.0`，除非用户明确覆盖。 +- theorem formalization、proof repair、proof completion 和 `sorry` completion。 +- patch review：检查 `sorry`、`admit`、新引入的 `axiom` 和 theorem statement drift。 +- 可选 Lean 专用 agent backend adapter 流程；当前实现的是由 coding agent 协调的 official `project-numina/numina-lean-agent` runtime 设置和调用。 +- proof blocked 时抽取最小失败 Lean fragment。 +- 借鉴 Lean 专用 agent 模式：theorem-state loop、premise retrieval、bounded proof search、失败记忆、validation oracle 和 minimal handoff。 + +Numina 是可选链路，也是当前唯一内置可部署 backend adapter。公共 CLI 不提供并行的 `numina-*` workflow；`doctor` 用于报告 readiness，`configure --setup-numina --project-name ` 用于在 review 后执行本地设置，默认位置为 `~/.ai4math/numina-runtime/`。只有当用户明确要求 `Numina`、`official Lean Agent`、批量 proof search 或外部 subagent run 时，才应进入 official Numina backend。 + +未来 backend adapter 可参考 `skills/lean-runtime/references/backend_adapter_checklist.md`，但在 deployment、readiness checks、调用、validation 和 failure triage 文档化前，不要写成已支持。 ## 仓库结构 ```text diff --git a/skills/lean-runtime/config/lean_agent.example.toml b/skills/lean-runtime/config/lean_agent.example.toml index 0a42f33..d402c66 100644 --- a/skills/lean-runtime/config/lean_agent.example.toml +++ b/skills/lean-runtime/config/lean_agent.example.toml @@ -9,7 +9,7 @@ managed_workspace_template = "math" reuse_managed_workspace = true workspace_key = "lean-toolchain" align_workspace_versions = true -preferred_toolchain = "auto" +preferred_toolchain = "leanprover/lean4:v4.28.0" preferred_mathlib_rev = "auto" allow_user_project_version_changes = false diff --git a/skills/lean-runtime/references/direct_lean_workflow.md b/skills/lean-runtime/references/direct_lean_workflow.md index a5fb44d..15506aa 100644 --- a/skills/lean-runtime/references/direct_lean_workflow.md +++ b/skills/lean-runtime/references/direct_lean_workflow.md @@ -33,7 +33,7 @@ Do not route creative proof search through helper commands. `prove`, `formalize` Prefer a user's existing Lake project when the target file is inside one. For standalone `.lean` files, use the reusable `${AI4MATH_HOME:-~/.ai4math}/lean-workspace` so Lean, Lake, and mathlib artifacts are shared across tasks and projects. -When a user project has its own `lean-toolchain` and mathlib revision, keep those versions unless the user explicitly approves a change. When creating a managed workspace, use the configured preferred toolchain or `auto`. +When a user project has its own `lean-toolchain` and mathlib revision, keep those versions unless the user explicitly approves a change. When creating a managed workspace, default to the AI4Math canonical toolchain `leanprover/lean4:v4.28.0` unless the user explicitly overrides it; use a versioned workspace for other standalone revisions instead of overwriting the canonical workspace. ## Good Stopping Points diff --git a/skills/lean-runtime/references/lean_runtime_configuration.md b/skills/lean-runtime/references/lean_runtime_configuration.md index 93544d1..e6b4930 100644 --- a/skills/lean-runtime/references/lean_runtime_configuration.md +++ b/skills/lean-runtime/references/lean_runtime_configuration.md @@ -28,22 +28,22 @@ Required default workflow tools are `git`, `python3`, `elan`, `lean`, and `lake` ## Reusable Lean Workspace -For standalone tasks, prefer `${AI4MATH_HOME:-~/.ai4math}/lean-workspace`. Create it once with: +For standalone tasks, prefer `${AI4MATH_HOME:-~/.ai4math}/lean-workspace`. This canonical managed workspace defaults to the AI4Math baseline toolchain `leanprover/lean4:v4.28.0`; use `--toolchain` only as an explicit override. Create it once with: ```bash -python skills/lean-runtime/scripts/ai4m_lean.py configure --cwd . --create-workspace --toolchain leanprover/lean4:v4.28.0 +python skills/lean-runtime/scripts/ai4m_lean.py configure --cwd . --create-workspace ``` Equivalent Lake commands: ```bash -lake new lean_workspace math -lake update -lake exe cache get -lake build +elan run leanprover/lean4:v4.28.0 lake new lean_workspace math +elan run leanprover/lean4:v4.28.0 lake update +elan run leanprover/lean4:v4.28.0 lake exe cache get +elan run leanprover/lean4:v4.28.0 lake build ``` -If a user project already has `lean-toolchain` and `lakefile.{lean,toml}`, use that project and do not change versions without approval. If a standalone task needs a different Lean/mathlib revision than the shared managed workspace, use a versioned workspace under `${AI4MATH_HOME:-~/.ai4math}/lean-workspaces/`. +If a user project already has `lean-toolchain` and `lakefile.{lean,toml}`, use that project and do not change versions without approval. If the canonical workspace already has `lake-manifest.json` and `.lake/`, reuse it instead of rerunning cache/build. If a standalone task needs a different Lean/mathlib revision than the shared managed workspace, use a versioned workspace under `${AI4MATH_HOME:-~/.ai4math}/lean-workspaces/` instead of overwriting `${AI4MATH_HOME:-~/.ai4math}/lean-workspace`. ## Local Config @@ -54,7 +54,7 @@ Machine-specific settings live in `.ai4math/lean_agent.local.toml` and should no workspace_mode = "reuse-managed" managed_workspace_path = "~/.ai4math/lean-workspace" align_workspace_versions = true -preferred_toolchain = "auto" +preferred_toolchain = "leanprover/lean4:v4.28.0" [agent] mode = "coding-agent" diff --git a/skills/lean-runtime/scripts/ai4m_lean.py b/skills/lean-runtime/scripts/ai4m_lean.py index 95e96ee..12da7ec 100644 --- a/skills/lean-runtime/scripts/ai4m_lean.py +++ b/skills/lean-runtime/scripts/ai4m_lean.py @@ -77,7 +77,7 @@ def build_parser() -> argparse.ArgumentParser: add_common(configure_parser) configure_parser.add_argument("--target", default=None) configure_parser.add_argument("--create-workspace", action="store_true") - configure_parser.add_argument("--toolchain", default=None, help="Optional Lean toolchain for managed workspace") + configure_parser.add_argument("--toolchain", default=None, help="Override the default AI4Math managed workspace toolchain") configure_parser.add_argument("--save-local", action="store_true") configure_parser.add_argument("--dry-run", action="store_true") configure_parser.add_argument("--setup-numina", action="store_true", help="Install/configure official Numina runtime after review") diff --git a/skills/lean-runtime/scripts/common.py b/skills/lean-runtime/scripts/common.py index addc80f..7026590 100644 --- a/skills/lean-runtime/scripts/common.py +++ b/skills/lean-runtime/scripts/common.py @@ -21,6 +21,7 @@ SKILL_ROOT = Path(__file__).resolve().parents[1] DEFAULT_CONFIG = SKILL_ROOT / "config" / "lean_agent.example.toml" ENV_KEY_RE = re.compile(r"^[A-Za-z_][A-Za-z0-9_]*$") +CANONICAL_LEAN_TOOLCHAIN = "leanprover/lean4:v4.28.0" def deep_merge(base: dict[str, Any], overlay: dict[str, Any]) -> dict[str, Any]: diff --git a/skills/lean-runtime/scripts/configure_lean.py b/skills/lean-runtime/scripts/configure_lean.py index badd59e..ed32bfa 100644 --- a/skills/lean-runtime/scripts/configure_lean.py +++ b/skills/lean-runtime/scripts/configure_lean.py @@ -5,7 +5,7 @@ from typing import Any from check_lean_project import find_project_root, read_mathlib_revision, read_toolchain -from common import ai4math_home, ensure_ai4math_gitignore, expand_path, read_config, run_command, update_local_toml +from common import CANONICAL_LEAN_TOOLCHAIN, ai4math_home, ensure_ai4math_gitignore, expand_path, read_config, run_command, update_local_toml from numina_runtime import execute_configure_plan, numina_readiness from tool_status import find_tool @@ -36,6 +36,19 @@ def _workspace_setup_commands(lake: str, toolchain: str | None, workspace: Path) return commands +def _effective_managed_toolchain(config: dict[str, Any], requested_toolchain: str | None) -> str: + if requested_toolchain is not None: + return requested_toolchain.strip() or CANONICAL_LEAN_TOOLCHAIN + configured = str(config.get("lean", {}).get("preferred_toolchain") or "").strip() + if configured and configured != "auto": + return configured + return CANONICAL_LEAN_TOOLCHAIN + + +def _workspace_needs_setup(workspace: Path) -> bool: + return not ((workspace / "lake-manifest.json").exists() and (workspace / ".lake").exists()) + + def _action_failed(action: dict[str, Any]) -> bool: return not action.get("skipped") and not action.get("recoverable") and not action.get("ok", False) @@ -113,6 +126,7 @@ def configure( config = read_config(cwd_path, config_path) lean = config.get("lean", {}) + effective_toolchain = _effective_managed_toolchain(config, toolchain) workspace = expand_path(lean.get("managed_workspace_path"), cwd_path) or (ai4math_home(cwd_path) / "lean-workspace") workspace_root_config = expand_path(lean.get("managed_workspace_root"), cwd_path) or (workspace.parent / "lean-workspaces") workspace_actions: list[dict[str, Any]] = [] @@ -123,14 +137,14 @@ def configure( created_path = parent / lake_project_name if dry_run: workspace_actions.append({ - "command": _lake_command(lake, toolchain, ["new", lake_project_name, "math"]), + "command": _lake_command(lake, effective_toolchain, ["new", lake_project_name, "math"]), "cwd": str(parent), "skipped": True, "reason": "dry_run", }) elif not workspace.exists(): parent.mkdir(parents=True, exist_ok=True) - created = run_command(_lake_command(lake, toolchain, ["new", lake_project_name, "math"]), cwd=parent) + created = run_command(_lake_command(lake, effective_toolchain, ["new", lake_project_name, "math"]), cwd=parent) if not created.get("ok") and find_project_root(created_path): created["recoverable"] = True created["recovered_by"] = "lake_project_files_created" @@ -153,8 +167,8 @@ def configure( "stdout": "", "stderr": "", }) - if not dry_run and find_project_root(workspace): - for command in _workspace_setup_commands(lake, toolchain, workspace): + if not dry_run and find_project_root(workspace) and _workspace_needs_setup(workspace): + for command in _workspace_setup_commands(lake, effective_toolchain, workspace): workspace_actions.append(run_command(command, cwd=workspace, timeout=1800)) workspace_info = _workspace_info(workspace) @@ -170,7 +184,7 @@ def configure( "reuse_managed_workspace": True, "workspace_key": "lean-toolchain", "align_workspace_versions": True, - "preferred_toolchain": toolchain or "auto", + "preferred_toolchain": effective_toolchain, "preferred_mathlib_rev": "auto", "allow_user_project_version_changes": False, }, diff --git a/skills/lean-runtime/scripts/verify_delivery.py b/skills/lean-runtime/scripts/verify_delivery.py index fe65ff4..5825210 100644 --- a/skills/lean-runtime/scripts/verify_delivery.py +++ b/skills/lean-runtime/scripts/verify_delivery.py @@ -253,6 +253,11 @@ def _lean_setup_entrypoint_check() -> dict[str, Any]: "When creating an isolated test directory or workspace", "suggest a safe default name", "use the default if the user has no naming preference", + "canonical managed workspace", + "AI4Math managed baseline toolchain `leanprover/lean4:v4.28.0`", + "reuse it instead of rebuilding or downloading again", + "Do not overwrite the canonical managed workspace", + "lean-workspaces//", "After successful setup or smoke-test validation", "Offer a short next-step menu", "inspect an existing Lean/Lake project", @@ -268,6 +273,10 @@ def _lean_setup_entrypoint_check() -> dict[str, Any]: repo_root_command_hits = [phrase for phrase in repo_root_commands if phrase in text] openai_required = [ "不要向用户索要 theorem target", + "已有 Lake 项目优先沿用项目自己的 lean-toolchain 和 lake-manifest", + "standalone 任务默认复用 ~/.ai4math/lean-workspace", + "AI4Math managed baseline leanprover/lean4:v4.28.0", + "避免重复下载和路径分裂", "setup 完成后主动给出下一步菜单", "所有实现应复用 lean-runtime", "默认 Lean/mathlib 环境配置不需要 API key", diff --git a/skills/lean-runtime/tests/test_cli.py b/skills/lean-runtime/tests/test_cli.py index 275a8dd..0dcdd7d 100644 --- a/skills/lean-runtime/tests/test_cli.py +++ b/skills/lean-runtime/tests/test_cli.py @@ -13,6 +13,7 @@ sys.path.insert(0, str(SKILL_ROOT / "scripts")) from ai4m_lean import EXIT_LEAN_FAILED, _exit_code # noqa: E402 +from common import CANONICAL_LEAN_TOOLCHAIN # noqa: E402 from verify_delivery import _lean_setup_entrypoint_check, _package_hygiene, _root_discovery_boundary_check # noqa: E402 CLI = SKILL_ROOT / "scripts" / "ai4m_lean.py" @@ -131,6 +132,34 @@ def test_configure_setup_numina_dry_run_outputs_official_upstream(self) -> None: self.assertIn("https://github.com/project-numina/numina-lean-agent", str(commands)) self.assertIn(["./setup.sh", "demo_project"], commands) + def test_configure_create_workspace_dry_run_defaults_to_canonical_toolchain(self) -> None: + with tempfile.TemporaryDirectory() as tmp: + root = Path(tmp) + result = subprocess.run( + [ + sys.executable, + str(CLI), + "configure", + "--cwd", + str(root), + "--create-workspace", + "--dry-run", + ], + text=True, + capture_output=True, + check=False, + env={ + **os.environ, + "AI4MATH_HOME": str(root / "shared-ai4math"), + "AI4MATH_LEAN_WORKSPACE": "", + "AI4MATH_LEAN_TOOLCHAIN": "", + }, + ) + self.assertIn(result.returncode, {0, 4}, result.stderr) + payload = json.loads(result.stdout) + command = payload["workspace_actions"][0]["command"] + self.assertEqual(command[1:4], ["run", CANONICAL_LEAN_TOOLCHAIN, "lake"]) + def test_lean_workspace_deploy_failure_uses_lean_exit_code(self) -> None: self.assertEqual( _exit_code({"ok": False, "status": "lean_workspace_setup_failed"}), diff --git a/skills/lean-runtime/tests/test_common_config.py b/skills/lean-runtime/tests/test_common_config.py index 67411ef..058e938 100644 --- a/skills/lean-runtime/tests/test_common_config.py +++ b/skills/lean-runtime/tests/test_common_config.py @@ -9,7 +9,7 @@ SCRIPTS = Path(__file__).resolve().parents[1] / "scripts" sys.path.insert(0, str(SCRIPTS)) -from common import ai4math_home, expand_path, load_toml, read_env_local, write_env_local # noqa: E402 +from common import CANONICAL_LEAN_TOOLCHAIN, ai4math_home, expand_path, load_toml, read_config, read_env_local, write_env_local # noqa: E402 class CommonConfigTests(unittest.TestCase): @@ -47,6 +47,25 @@ def test_ai4math_home_honors_environment_override(self) -> None: self.assertEqual(result, custom) + def test_default_config_uses_canonical_toolchain(self) -> None: + with tempfile.TemporaryDirectory() as tmp: + root = Path(tmp) + + with patch.dict("os.environ", {"AI4MATH_LEAN_TOOLCHAIN": ""}, clear=False): + config = read_config(root) + + self.assertEqual(config["lean"]["preferred_toolchain"], CANONICAL_LEAN_TOOLCHAIN) + + def test_environment_can_override_canonical_toolchain(self) -> None: + with tempfile.TemporaryDirectory() as tmp: + root = Path(tmp) + override = "leanprover/lean4:v4.26.0" + + with patch.dict("os.environ", {"AI4MATH_LEAN_TOOLCHAIN": override}, clear=False): + config = read_config(root) + + self.assertEqual(config["lean"]["preferred_toolchain"], override) + def test_write_env_local_updates_values_and_is_ignored(self) -> None: with tempfile.TemporaryDirectory() as tmp: root = Path(tmp) diff --git a/skills/lean-runtime/tests/test_configure_lean.py b/skills/lean-runtime/tests/test_configure_lean.py index 1d5c15f..908e85a 100644 --- a/skills/lean-runtime/tests/test_configure_lean.py +++ b/skills/lean-runtime/tests/test_configure_lean.py @@ -10,7 +10,7 @@ SCRIPTS = Path(__file__).resolve().parents[1] / "scripts" sys.path.insert(0, str(SCRIPTS)) -from common import load_toml # noqa: E402 +from common import CANONICAL_LEAN_TOOLCHAIN, load_toml # noqa: E402 from configure_lean import configure, inspect_environment # noqa: E402 @@ -52,6 +52,56 @@ def test_save_local_writes_lean_agent_config(self) -> None: self.assertEqual(local["lean"]["preferred_toolchain"], "leanprover/lean4:v4.28.0") self.assertIn("lean_agent.local.toml", (root / ".ai4math" / ".gitignore").read_text()) + def test_save_local_defaults_to_canonical_toolchain(self) -> None: + with tempfile.TemporaryDirectory() as tmp: + root = Path(tmp) + + with patch.dict(os.environ, {"AI4MATH_HOME": str(root / "shared-ai4math"), "AI4MATH_LEAN_TOOLCHAIN": ""}, clear=False): + os.environ["AI4MATH_LEAN_WORKSPACE"] = "" + result = configure(root, save_local=True) + local = load_toml(root / ".ai4math" / "lean_agent.local.toml") + + self.assertFalse(result["ok"]) + self.assertEqual(local["lean"]["preferred_toolchain"], CANONICAL_LEAN_TOOLCHAIN) + + def test_create_workspace_dry_run_uses_canonical_toolchain(self) -> None: + with tempfile.TemporaryDirectory() as tmp: + root = Path(tmp) + + with patch.dict(os.environ, {"AI4MATH_HOME": str(root / "shared-ai4math"), "AI4MATH_LEAN_TOOLCHAIN": ""}, clear=False), \ + patch("configure_lean.find_tool", side_effect=lambda tool: f"/usr/bin/{tool}"): + os.environ["AI4MATH_LEAN_WORKSPACE"] = "" + result = configure(root, create_workspace=True, dry_run=True) + + self.assertEqual(result["workspace_actions"][0]["command"], [ + "/usr/bin/elan", + "run", + CANONICAL_LEAN_TOOLCHAIN, + "lake", + "new", + "lean_workspace", + "math", + ]) + + def test_complete_managed_workspace_is_reused_without_rebuild(self) -> None: + with tempfile.TemporaryDirectory() as tmp: + root = Path(tmp) + workspace = root / "shared-ai4math" / "lean-workspace" + workspace.mkdir(parents=True) + (workspace / "lean-toolchain").write_text(f"{CANONICAL_LEAN_TOOLCHAIN}\n", encoding="utf-8") + (workspace / "lakefile.toml").write_text('name = "lean_workspace"\n', encoding="utf-8") + (workspace / "lake-manifest.json").write_text('{"packages":[]}\n', encoding="utf-8") + (workspace / ".lake").mkdir() + + with patch.dict(os.environ, {"AI4MATH_HOME": str(root / "shared-ai4math"), "AI4MATH_LEAN_TOOLCHAIN": ""}, clear=False), \ + patch("configure_lean.run_command") as run_command: + os.environ["AI4MATH_LEAN_WORKSPACE"] = "" + result = configure(root, create_workspace=True) + + self.assertTrue(result["ok"]) + self.assertEqual(result["workspace_actions"][0]["command"], ["reuse", str(workspace)]) + run_command.assert_not_called() + def test_workspace_creation_failure_is_reported_as_lean_setup_failure(self) -> None: with tempfile.TemporaryDirectory() as tmp: root = Path(tmp) diff --git a/skills/lean-setup/SKILL.md b/skills/lean-setup/SKILL.md index be22520..3b8a7d9 100644 --- a/skills/lean-setup/SKILL.md +++ b/skills/lean-setup/SKILL.md @@ -16,8 +16,8 @@ The shared implementation lives in `../lean-runtime/`. This skill must reuse the 3. If `elan`, `lean`, or `lake` is missing, explain the required Lean installation step first. Install Lean through the official `elan` channel appropriate for the user's OS after approval; `lean` and `lake` should come from the `elan` toolchain rather than a repository-local copy. 4. Prefer an existing Lake project when the user points to one. 5. When creating an isolated test directory or workspace, suggest a safe default name and let the user confirm or rename it; use the default if the user has no naming preference. -6. For standalone future Lean work, create or reuse `${AI4MATH_HOME:-~/.ai4math}/lean-workspace`. -7. Create the workspace only after explaining that Lean/mathlib artifacts may be downloaded or built. +6. For standalone future Lean work, create or reuse the canonical managed workspace `${AI4MATH_HOME:-~/.ai4math}/lean-workspace` with the AI4Math managed baseline toolchain `leanprover/lean4:v4.28.0`. +7. Create the workspace only after explaining that Lean/mathlib artifacts may be downloaded or built. If the canonical workspace already exists and is complete, reuse it instead of rebuilding or downloading again. 8. Run the bundled smoke test after setup. 9. Report the installed tools, workspace path, Lean toolchain, mathlib revision when available, smoke-test result, and any remaining action. 10. After successful setup or smoke-test validation, do not end passively. Offer a short next-step menu and recommend one default next action. @@ -52,6 +52,7 @@ Use `--dry-run` before setup when the user wants to review commands. - Do not create a second setup implementation. - Do not change a user project's `lean-toolchain` or mathlib revision without approval. +- Do not overwrite the canonical managed workspace for a different Lean/mathlib revision. Use `${AI4MATH_HOME:-~/.ai4math}/lean-workspaces//` only when the user explicitly needs a different standalone version. - Do not require API keys for Lean/mathlib workspace setup. - Do not configure or call official Numina unless the user explicitly asks for that optional backend. - Do not commit machine-specific paths, downloaded runtime state, or secrets. diff --git a/skills/lean-setup/agents/openai.yaml b/skills/lean-setup/agents/openai.yaml index 81dee2e..c40b335 100644 --- a/skills/lean-setup/agents/openai.yaml +++ b/skills/lean-setup/agents/openai.yaml @@ -1,3 +1,3 @@ display_name: Lean Setup short_description: Lean 4, elan, lake, and reusable mathlib workspace setup for coding agents. -default_prompt: 请默认使用中文，并主动完成 Lean 环境配置引导；仅当用户明确使用其他语言时切换。该入口仅用于 setup-only 任务：检查或安装 Lean/elan/lake，创建或复用带 mathlib 的共享工作区，运行 smoke-test，并报告 workspace 路径、toolchain、mathlib revision、验证结果与剩余动作。不要向用户索要 theorem target。setup 完成后主动给出下一步菜单，例如检查 Lean/Lake 项目、运行或解释 smoke theorem、修 Lean 文件或补 sorry、形式化自然语言/LaTeX 命题，或继续 setup-only readiness；推荐一个默认下一步。所有实现应复用 lean-runtime 的 helper CLI 与 runtime references，不复制第二套配置逻辑，也不要把 lean-formalization 当作 setup 的实现依赖。默认 Lean/mathlib 环境配置不需要 API key；只有在用户明确要求 optional official Numina backend 时，才说明凭据需求并请求批准，不要把 Numina 放进默认下一步。配置完成后，如用户要进行形式化、proof repair、sorry completion 或 Numina proof search，应交接到 lean-formalization。 +default_prompt: 请默认使用中文，并主动完成 Lean 环境配置引导；仅当用户明确使用其他语言时切换。该入口仅用于 setup-only 任务：检查或安装 Lean/elan/lake，创建或复用带 mathlib 的共享工作区，运行 smoke-test，并报告 workspace 路径、toolchain、mathlib revision、验证结果与剩余动作。不要向用户索要 theorem target。已有 Lake 项目优先沿用项目自己的 lean-toolchain 和 lake-manifest；standalone 任务默认复用 ~/.ai4math/lean-workspace，并使用 AI4Math managed baseline leanprover/lean4:v4.28.0，避免重复下载和路径分裂；不同 standalone 版本才使用 ~/.ai4math/lean-workspaces/。setup 完成后主动给出下一步菜单，例如检查 Lean/Lake 项目、运行或解释 smoke theorem、修 Lean 文件或补 sorry、形式化自然语言/LaTeX 命题，或继续 setup-only readiness；推荐一个默认下一步。所有实现应复用 lean-runtime 的 helper CLI 与 runtime references，不复制第二套配置逻辑，也不要把 lean-formalization 当作 setup 的实现依赖。默认 Lean/mathlib 环境配置不需要 API key；只有在用户明确要求 optional official Numina backend 时，才说明凭据需求并请求批准，不要把 Numina 放进默认下一步。配置完成后，如用户要进行形式化、proof repair、sorry completion 或 Numina proof search，应交接到 lean-formalization。