lemmascript - npm Package Compare versions

Comparing version 0.5.11 to 0.5.12

package.json

 {
   "name": "lemmascript",
-  "version": "0.5.11",
+  "version": "0.5.12",
   "description": "A verification toolchain for TypeScript — generates Lean 4 or Dafny from annotated TS",
@@ -5,0 +5,0 @@ "type": "module",

README.md

@@ -48,3 +48,3 @@ # LemmaScript (Tech Preview)
 ```sh
-npm install lemmascript
+npm install -g lemmascript
 ```
@@ -71,7 +71,11 @@
 ```sh
-npx lsc gen --backend=dafny src/myModule.ts
-npx lsc check --backend=dafny src/myModule.ts
-npx lsc regen --backend=dafny src/myModule.ts
+lsc gen --backend=dafny src/myModule.ts
+lsc check --backend=dafny src/myModule.ts
+lsc regen --backend=dafny src/myModule.ts
 ```
 
+With no file argument, `lsc check` batches over `LemmaScript-files.txt` (one `filepath [timeout] [extra dafny flags…]` per line — the list `tools/check.sh` runs in CI).
+
+From a sibling source checkout, the equivalent of `lsc` is `npx tsx ../LemmaScript/tools/src/lsc.ts` — no build step, toolchain edits apply immediately.
+
 The Dafny backend generates two files per TS source: `foo.dfy.gen` (always regeneratable) and `foo.dfy` (source of truth, with LLM/user proof additions). The diff between them must be additions-only.
@@ -82,3 +86,3 @@
 ```sh
-npx lsc gen --backend=lean src/myModule.ts
+lsc gen --backend=lean src/myModule.ts
 lake build
@@ -85,0 +89,0 @@ ```

tools/dist/lsc.js

@@ -8,3 +8,5 @@ #!/usr/bin/env node
 import { Project, ScriptTarget } from "ts-morph";
-import { existsSync } from "fs";
+import { existsSync, readFileSync } from "fs";
+import { execFileSync } from "child_process";
+import { createRequire } from "module";
 import path from "path";
@@ -24,16 +26,40 @@ import { extractModule } from "./extract.js";
     const args = process.argv.slice(2);
-    // `lsc claimcheck …` forwards verbatim to the lemmascript-claimcheck CLI
-    // (a dependency; its cli reads the rewritten process.argv).
+    // `lsc claimcheck <file.ts> …` forwards verbatim to the lemmascript-claimcheck
+    // CLI (a dependency; its cli reads the rewritten process.argv). With no
+    // leading <file.ts>, batch: one satellite run per LemmaScript-files.txt entry,
+    // flags passed through unchanged — the loop is owned here, the satellite
+    // stays single-file.
     if (args[0] === "claimcheck") {
-        process.argv = [process.argv[0], "lemmascript-claimcheck", ...args.slice(1)];
-        import("lemmascript-claimcheck/cli").catch((err) => {
-            const code = err?.code;
-            if (code === "ERR_MODULE_NOT_FOUND" || code === "ERR_PACKAGE_PATH_NOT_EXPORTED") {
-                console.error("`lsc claimcheck` needs lemmascript-claimcheck >= 0.2.0; reinstall with: npm i -g lemmascript");
-            }
-            else {
+        const rest = args.slice(1);
+        const missing = () => {
+            console.error("`lsc claimcheck` needs lemmascript-claimcheck >= 0.2.0; reinstall with: npm i -g lemmascript");
+            process.exit(1);
+        };
+        if (rest[0] && !rest[0].startsWith("-")) {
+            process.argv = [process.argv[0], "lemmascript-claimcheck", ...rest];
+            import("lemmascript-claimcheck/cli").catch((err) => {
+                const code = err?.code;
+                if (code === "ERR_MODULE_NOT_FOUND" || code === "ERR_PACKAGE_PATH_NOT_EXPORTED")
+                    missing();
                 console.error(err instanceof Error ? err.message : String(err));
+                process.exit(1);
+            });
+            return;
+        }
+        let cli;
+        try {
+            cli = createRequire(import.meta.url).resolve("lemmascript-claimcheck/cli");
+        }
+        catch {
+            missing();
+            return;
+        }
+        for (const e of readEntries()) {
+            try {
+                execFileSync(process.execPath, [cli, e.file, ...rest], { stdio: "inherit" });
             }
-            process.exit(1);
-        });
+            catch {
+                process.exit(1);
+            }
+        }
         return;
@@ -64,8 +90,59 @@ }
     }
+    // --slow (batch mode only): verify every entry with its own timeout instead
+    // of degrading slow ones to gen-check.
+    let slow = false;
+    const slowIdx = args.indexOf("--slow");
+    if (slowIdx >= 0) {
+        slow = true;
+        args.splice(slowIdx, 1);
+    }
     const [cmd, filePath] = args;
-    if (!cmd || !filePath) {
+    if (!cmd) {
         console.error("Usage: lsc <gen|check|regen|extract|info> [--backend=lean|dafny] <file.ts>");
-        console.error("       lsc claimcheck <file.ts> [flags…]   (forwards to lemmascript-claimcheck)");
+        console.error("       lsc <gen|gen-check|check> [--backend=…] [--slow]   (no file: batch over LemmaScript-files.txt)");
+        console.error("       lsc claimcheck [<file.ts>] [flags…]   (forwards to lemmascript-claimcheck)");
         process.exit(1);
     }
+    if (!filePath) {
+        runBatch(cmd, backend, slow);
+        return;
+    }
+    runFile(cmd, filePath, backend, timeLimit, extraFlags);
+}
+// LemmaScript-files.txt, parsed: `filepath [timeout_in_seconds] [extra dafny
+// flags…]` per line; no timeout = Dafny default. Exits if the file is absent.
+function readEntries() {
+    if (!existsSync("LemmaScript-files.txt")) {
+        console.error("No file given and no LemmaScript-files.txt found.");
+        process.exit(1);
+    }
+    return readFileSync("LemmaScript-files.txt", "utf8")
+        .split("\n").map(s => s.trim()).filter(Boolean)
+        .map(entry => {
+        const [file, second, ...rest] = entry.split(/\s+/);
+        const timeout = second && /^[1-9]\d*$/.test(second) ? parseInt(second) : undefined;
+        const flags = (timeout === undefined ? [second, ...rest] : rest).filter(Boolean).join(" ") || undefined;
+        return { file, timeout, flags };
+    });
+}
+// Batch over LemmaScript-files.txt. `check` entries with a timeout above 60s
+// (the CI limit) are gen-check only, unless --slow. Fail-fast: the first
+// failing entry exits. tools/check.sh drives this from source;
+// installed-package consumers run `lsc check`.
+function runBatch(cmd, backend, slow) {
+    if (cmd !== "gen" && cmd !== "gen-check" && cmd !== "check") {
+        console.error(`No file given, and batch mode supports gen|gen-check|check (not ${cmd}).`);
+        process.exit(1);
+    }
+    for (const e of readEntries()) {
+        if (cmd === "check" && backend === "dafny" && !slow && e.timeout !== undefined && e.timeout > 60) {
+            console.log(`=== ${path.basename(e.file)} (timeout ${e.timeout}s > 60s, gen-check only) ===`);
+            runFile("gen-check", e.file, backend, undefined, undefined);
+        }
+        else {
+            runFile(cmd, e.file, backend, e.timeout, e.flags);
+        }
+    }
+}
+function runFile(cmd, filePath, backend, timeLimit, extraFlags) {
     const absPath = path.resolve(filePath);
@@ -72,0 +149,0 @@ if (!existsSync(absPath)) {

New alerts

Debug access

Supply chain risk

Uses debug, reflection and dynamic code execution features.

Filesystem access

Supply chain risk

Accesses the file system, and could potentially read sensitive data.

Fixed alerts

Filesystem access

Supply chain risk

Accesses the file system, and could potentially read sensitive data.

Improved metrics

Total package byte prevSize

606461

0.59%

Lines of code

11901

0.65%

Number of lines in readme file

120

3.45%

Worsened metrics

Number of low supply chain risk alerts

6

20%

Number of medium supply chain risk alerts

3

50%

No dependency changes