allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-07-31 03:05:21 +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 48da4d058c
commit d50699b619
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.
//!
//! 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.