lean-agentic 0.3.4: working root entry point, quiet MCP stdout (fixes #5)

.github/workflows/ci.yml

@@ -39,7 +39,11 @@ jobs:
           timeout 60 node -e "require('./dist/node.js').createDemo().createIdentity()"
       - name: Audit runtime dependencies
         run: npm audit --omit=dev --audit-level=high
-      - run: npm pack --dry-run --ignore-scripts
+      - name: Pack, install the tarball into a temp project, check every entry point and MCP stdio
+        run: |
+          npm pack --ignore-scripts --pack-destination "$RUNNER_TEMP"
+          version=$(node -p "require('./package.json').version")
+          timeout 600 node scripts/check-package.mjs "$RUNNER_TEMP/lean-agentic-$version.tgz"
 
   rust:
     name: cargo test

leanr-wasm/src/lib.rs

@@ -7,8 +7,26 @@ use lean_agentic::{Arena, Environment, SymbolTable};
 use lean_agentic::level::LevelArena;
 use lean_agentic::term::{Binder, BinderInfo};
 use wasm_bindgen::prelude::*;
+use std::sync::atomic::{AtomicBool, Ordering};
 use web_sys::console;
 
+/// Diagnostic logging is off by default. When on, it goes to `console.error`
+/// (stderr under Node), so it never mixes with stdout, which the MCP server
+/// uses for JSON-RPC.
+static DEBUG: AtomicBool = AtomicBool::new(false);
+
+fn debug_log(msg: &str) {
+    if DEBUG.load(Ordering::Relaxed) {
+        console::error_1(&msg.into());
+    }
+}
+
+/// Turn diagnostic logging on or off (off by default).
+#[wasm_bindgen(js_name = setDebug)]
+pub fn set_debug(enabled: bool) {
+    DEBUG.store(enabled, Ordering::Relaxed);
+}
+
 /// Demo struct showing hash-consing performance in WASM
 #[wasm_bindgen]
 pub struct LeanDemo {
@@ -24,7 +42,7 @@ impl LeanDemo {
     /// Create a new Lean demo instance
     #[wasm_bindgen(constructor)]
     pub fn new() -> Self {
-        console::log_1(&"Initializing Lean-Agentic WASM...".into());
+        debug_log("Initializing Lean-Agentic WASM...");
 
         Self {
             arena: Arena::new(),
@@ -41,7 +59,7 @@ impl LeanDemo {
     pub fn create_variable(&mut self, index: u32) -> bool {
         let term = self.arena.mk_var(index);
         self.term_counter += 1;
-        console::log_1(&format!("Created variable with index {} -> TermId {:?}", index, term).into());
+        debug_log(&format!("Created variable with index {} -> TermId {:?}", index, term));
         true
     }
 
@@ -54,10 +72,10 @@ impl LeanDemo {
 
         let same = var1 == var2;
 
-        console::log_1(&format!(
+        debug_log(&format!(
             "Hash-consing test: var1={:?}, var2={:?}, same={}",
             var1, var2, same
-        ).into());
+        ));
 
         same
     }
@@ -77,7 +95,7 @@ impl LeanDemo {
         let level_zero = self.levels.zero();
         let type_term = self.arena.mk_sort(level_zero);
         self.term_counter += 1;
-        console::log_1(&format!("Created Type: {:?}", type_term).into());
+        debug_log(&format!("Created Type: {:?}", type_term));
         true
     }
 
@@ -100,7 +118,7 @@ impl LeanDemo {
         let lambda = self.arena.mk_lam(binder, var_x);
 
         self.term_counter += 3;
-        console::log_1(&format!("Created identity function: λx:Type. x = {:?}", lambda).into());
+        debug_log(&format!("Created identity function: λx:Type. x = {:?}", lambda));
         true
     }
 

npm/lean-agentic/README.md

@@ -549,7 +549,11 @@ demo.createApplication();
 demo.demonstrateHashConsing();
 ```
 
-### Bundler API
+### Root entry point (Node.js)
+
+The root entry point is the Node.js build (same API as `lean-agentic/node`, plus `init()`). In the browser, use `lean-agentic/web`.
+
+The WASM module is silent by default. Set `LEAN_AGENTIC_DEBUG=1` (or call `setDebug(true)`) to print its diagnostic logs; they go to stderr, so they never mix with the MCP server's JSON-RPC on stdout.
 
 ```javascript
 import { init, createDemo } from 'lean-agentic';
@@ -610,11 +614,9 @@ console.timeEnd('Hash-consed equality');
 
 | Platform | Support | Import |
 |----------|---------|--------|
-| Node.js 18+ | ✅ | `lean-agentic/node` |
+| Node.js 18+ | ✅ | `lean-agentic` or `lean-agentic/node` |
 | Browser (ESM) | ✅ | `lean-agentic/web` |
-| Webpack | ✅ | `lean-agentic` |
-| Vite | ✅ | `lean-agentic` |
-| Rollup | ✅ | `lean-agentic` |
+| Webpack / Vite / Rollup (browser) | ✅ | `lean-agentic/web` |
 | Deno | ✅ | `npm:lean-agentic` |
 | Bun | ✅ | `lean-agentic` |
 
@@ -671,7 +673,6 @@ cd lean-agentic
 cd leanr-wasm
 wasm-pack build --target nodejs --out-dir ../npm/lean-agentic/wasm-node
 wasm-pack build --target web --out-dir ../npm/lean-agentic/wasm-web
-wasm-pack build --target bundler --out-dir ../npm/lean-agentic/wasm
 
 # Install dependencies
 cd ../npm/lean-agentic

npm/lean-agentic/cli/index.js

@@ -164,9 +164,13 @@ mcp
     console.error('Tools: 5 | Resources: 2 | Prompts: 2');
     console.error('Ready for Claude Code integration\n');
 
-    // Launch the MCP server
+    // Launch the MCP server. Requiring server.js alone does not start it
+    // (it only auto-starts when run directly), so call startServer().
     const serverPath = join(__dirname, '../mcp/server.js');
-    require(serverPath);
+    require(serverPath).startServer().catch((error) => {
+      process.stderr.write(`Fatal error: ${error}\n`);
+      process.exit(1);
+    });
   });
 
 mcp

npm/lean-agentic/dist/index.d.ts

@@ -1,73 +1,31 @@
 /**
  * lean-agentic TypeScript definitions
  *
- * Hash-consed dependent types with 150x faster equality
+ * Hash-consed dependent types with 150x faster equality. Under Node.js the
+ * root entry point has the same API as `lean-agentic/node`, plus `init()`.
+ * Browsers should use `lean-agentic/web`.
  *
  * @module lean-agentic
  * @author ruv.io
  * @license Apache-2.0
  */
 
-/**
- * Initialize the WASM module
- */
-export function init(): Promise<void>;
+import { LeanDemo, createDemo, quickStart, setDebug, wasm } from './node';
 
-/**
- * Main interface for lean-agentic theorem prover
- */
-export class LeanDemo {
-  constructor();
-
-  /**
-   * Create identity function: λx:Type. x
-   * @returns JSON representation of the identity function
-   */
-  createIdentity(): string;
-
-  /**
-   * Create and verify an application
-   * @returns JSON representation of the application
-   */
-  createApplication(): string;
-
-  /**
-   * Demonstrate hash-consing by creating identical terms
-   * @returns JSON showing term equality
-   */
-  demonstrateHashConsing(): string;
-}
+export { LeanDemo, createDemo, quickStart, setDebug, wasm };
 
 /**
- * Create a new LeanDemo instance
+ * Kept for API compatibility. Resolves immediately: the Node WASM build is
+ * ready as soon as it is loaded.
  */
-export function createDemo(): LeanDemo;
-
-/**
- * Quick start: Create identity function
- */
-export function quickStart(): Promise<string>;
-
-/**
- * WASM module exports
- */
-export namespace wasm {
-  export class LeanDemo {
-    constructor();
-    create_identity(): string;
-    create_application(): string;
-    demonstrate_hash_consing(): string;
-  }
-}
+export function init(): Promise<void>;
 
-/**
- * Default export
- */
 declare const _default: {
   init: typeof init;
   LeanDemo: typeof LeanDemo;
   createDemo: typeof createDemo;
   quickStart: typeof quickStart;
+  setDebug: typeof setDebug;
   wasm: typeof wasm;
 };
 

npm/lean-agentic/dist/index.js

@@ -1,81 +1,29 @@
 /**
  * lean-agentic - Hash-consed dependent types with 150x faster equality
  *
+ * Root entry point. Under Node.js this is the same API as `lean-agentic/node`,
+ * plus an `init()` that resolves immediately (the Node WASM build loads
+ * synchronously). Browsers should use `lean-agentic/web`.
+ *
  * @module lean-agentic
  * @author ruv.io
  * @license Apache-2.0
  */
 
-const wasm = require('../wasm/leanr_wasm.js');
+const node = require('./node.js');
 
 /**
- * Initialize the WASM module
+ * Kept for API compatibility: the Node WASM build is ready as soon as it is
+ * required, so there is nothing to wait for.
  * @returns {Promise<void>}
  */
-export async function init() {
-  // WASM is already initialized when imported
-  return Promise.resolve();
-}
-
-/**
- * LeanDemo - Main interface for lean-agentic
- */
-class LeanDemo {
-  constructor() {
-    this._inner = new wasm.LeanDemo();
-  }
-
-  /**
-   * Create identity function: λx:Type. x
-   * @returns {string} JSON representation of the identity function
-   */
-  createIdentity() {
-    return this._inner.create_identity();
-  }
-
-  /**
-   * Create and verify an application
-   * @returns {string} JSON representation of the application
-   */
-  createApplication() {
-    return this._inner.create_application();
-  }
-
-  /**
-   * Demonstrate hash-consing by creating identical terms
-   * @returns {string} JSON showing term equality
-   */
-  demonstrateHashConsing() {
-    return this._inner.demonstrate_hash_consing();
-  }
-}
-
-/**
- * Create a new LeanDemo instance
- * @returns {LeanDemo}
- */
-function createDemo() {
-  return new LeanDemo();
-}
-
-/**
- * Quick start: Create identity function
- * @returns {Promise<string>}
- */
-export async function quickStart() {
-  await init();
-  const demo = createDemo();
-  return demo.createIdentity();
-}
-
-// Re-export WASM types
-module.exports = { wasm };
+async function init() {}
 
-// Default export
 module.exports = {
   init,
-  LeanDemo,
-  createDemo,
-  quickStart,
-  wasm
+  LeanDemo: node.LeanDemo,
+  createDemo: node.createDemo,
+  quickStart: node.quickStart,
+  setDebug: node.setDebug,
+  wasm: node.wasm
 };