From d50699b619eb1acef83a2e26ccf9e1ee3e487142 Mon Sep 17 00:00:00 2001 From: Allaun Silverfox <28494262+allaunthefox@users.noreply.github.com> Date: Tue, 26 May 2026 18:06:56 -0500 Subject: [PATCH] docs(runtime): update Lean manifest cmd example to ENE surface toolsJson --- .../claw/rust/crates/runtime/src/lean_mcp_manifest.rs | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/1-Distributed-Systems/agents/claw/rust/crates/runtime/src/lean_mcp_manifest.rs b/1-Distributed-Systems/agents/claw/rust/crates/runtime/src/lean_mcp_manifest.rs index 0db5f4b8..45fc0153 100644 --- a/1-Distributed-Systems/agents/claw/rust/crates/runtime/src/lean_mcp_manifest.rs +++ b/1-Distributed-Systems/agents/claw/rust/crates/runtime/src/lean_mcp_manifest.rs @@ -1,7 +1,7 @@ //! Lean-first MCP manifest loader. //! //! This is a boundary shim: it loads the published MCP tool list from a Lean-owned -//! JSON manifest (generated by `Semantics.McpSurfaceManifest`). +//! JSON manifest (generated by Lean). //! //! Semantics are NOT defined here: this module only parses JSON into runtime //! `McpTool` descriptors. @@ -77,8 +77,10 @@ pub fn tools_from_lean_command(command: &[String]) -> Result, Strin /// Load the Lean manifest using environment variables. /// -/// - `CLAW_LEAN_MCP_MANIFEST_CMD`: a JSON array of strings, e.g. -/// `["bash","-lc","cd 0-Core-Formalism/otom/tools/lean/Semantics && lake env lean -R Semantics -E 'import Semantics.McpSurfaceManifest; open Semantics.McpSurfaceManifest; #eval instanceToolsJson'"]` +/// - `CLAW_LEAN_MCP_MANIFEST_CMD`: a JSON array of strings. +/// +/// Example (ENE context surface): +/// `["bash","-lc","cd 0-Core-Formalism/otom/tools/lean/Semantics && lake env lean -R Semantics -E 'import Semantics.EneContextSurface; open Semantics.EneContextSurface; #eval toolsJson'"]` /// /// This stays shim-only: the env var provides *how* to invoke Lean; the manifest /// itself is the tool truth.