docs(runtime): update Lean manifest cmd example to ENE surface toolsJson

This commit is contained in:
Allaun Silverfox 2026-05-26 18:06:56 -05:00
parent 7574b37aef
commit 2f6cc3aa88

View file

@ -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<Vec<McpTool>, 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.