allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-08-17 03:20:34 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

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

Browse source
This commit is contained in:
Allaun Silverfox 2026-05-26 18:06:56 -05:00
parent 67d396bc9e
commit 7f8f183c21
1 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
1-Distributed-Systems/agents/claw/rust/crates/runtime/src/lean_mcp_manifest.rs
View file

@ -1,7 +1,7 @@
//! Lean-first MCP manifest loader. //! Lean-first MCP manifest loader.
//! //!
//! This is a boundary shim: it loads the published MCP tool list from a Lean-owned //! 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 //! Semantics are NOT defined here: this module only parses JSON into runtime
//! `McpTool` descriptors. //! `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. /// Load the Lean manifest using environment variables.
/// ///
/// - `CLAW_LEAN_MCP_MANIFEST_CMD`: a JSON array of strings, e.g. /// - `CLAW_LEAN_MCP_MANIFEST_CMD`: a JSON array of strings.
/// `["bash","-lc","cd 0-Core-Formalism/otom/tools/lean/Semantics && lake env lean -R Semantics -E 'import Semantics.McpSurfaceManifest; open Semantics.McpSurfaceManifest; #eval instanceToolsJson'"]` ///
/// 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 /// This stays shim-only: the env var provides *how* to invoke Lean; the manifest
/// itself is the tool truth. /// itself is the tool truth.