Run Lean3 in NodeJS

Stream: new members

[Phillip Ted]

Hello.
Recently I'm trying to run the Lean theorem prover on nodejs. (Due to some reasons I must use the Emscripten build of Lean rather than the binary version) I have read the project lean-client-js and tried to init the server with Mathlib:

const FS = require("browserfs/dist/node/core/FS").default;
const ZipFS = require("browserfs/dist/node/backend/ZipFS").default;
const EmscriptenFS =
  require("browserfs/dist/node/generic/emscripten_fs").default;
const fs = require("fs");
// Path to core library
const zipLib = fs.readFileSync("library.zip");
const loadJs = new Promise((r, e) => {
    // Emscripten build of Lean
  Object.assign(Module, require("./lean_js_js"));
  r(null);
});

async function init() {
  const Module = {};
  const loadJs = new Promise((r, e) => {
    Object.assign(Module, require("./lean_js_js"));
    r(null);
  });
  await Promise.all([loadJs]);
  const libraryFS = await new Promise((resolve, reject) =>
    ZipFS.Create({ zipData: zipLib }, (err, res) =>
      err ? reject(err) : resolve(res)
    )
  );

  const BrowserFS = new FS();
  BrowserFS.initialize(libraryFS);
  const BFS = new EmscriptenFS(Module.FS, PATH, ERROR_CODE, BrowserFS);
  Module.FS.createPath(Module.FS.root, "library", true, true);
  Module.FS.mount(BFS, { root: "/" }, "/library");
  Module._lean_init();
  console.log("lean server initialized.");
  return Module;
}

However, when I attempted to sync a test file (Check the attachment index.js for details) I got the error:

{"msgs":[{"caption":"","file_name":"test.lean","pos_col":0,"pos_line":1,"severity":"error","text":"file '/library/init/default.olean' not found"}],"response":"all_messages"}

I'm sure that the file exists. Can anyone tell me what's wrong here?

Thanks in advance!

[Scott Morrison]

Unfortunately I'm not sure you'll get much traction on this, as Lean 3 is at end-of-life, and everyone is transitioning to using Lean 4. There is currently no way to run Lean 4 inside a javascript environment, although there has been discussion at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/wasm.20nix.20emscripten.20build/near/271113368

[Eric Wieser]

One thing you could try is reading the file from the FS object manually and verifying that works

[Phillip Ted]

Eric Wieser said:

One thing you could try is reading the file from the FS object manually and verifying that works

I tried this and it worked well. But I still got the same error when sync the lean file