lemmascript - npm Package Compare versions

Comparing version 0.5.14 to 0.5.15

package.json

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

tools/dist/lean-emit.js

 /**
- * Lean emitter — IR → Lean text.
- * No logic, no type decisions — just serialization.
+ * Lean emitter — IR → Lean text. Beyond serialization it makes type-driven
+ * decisions: Bool-vs-Prop connectives, dropping Repr/DecidableEq for
+ * opaque-tainted types, discriminator/destructor lowering, method dispatch,
+ * and support-import selection.
  */
@@ -763,2 +765,16 @@ import { anyExpr, usesNameInDecl, patternBinders } from "./ir.js";
 // ── File emission ────────────────────────────────────────────
+/** Reset per-module emitter state. Call once per module before the types file
+ *  (not between types and def — the def file reads the types file's registries). */
+export function resetLeanModule() {
+    _resultName = "res";
+    _unionCtors.clear();
+    _opaqueNames.clear();
+    _opaqueNames.add("Unknown");
+    _typeRefs.clear();
+    _taintedTypes.clear();
+    _needsJSString = false;
+    _needsUnknown = false;
+    _unknownEmitted = false;
+    _boolCtx = false;
+}
 export function emitLeanFile(file) {
@@ -765,0 +781,0 @@ _needsJSString = false;

tools/dist/lsc.js

@@ -18,3 +18,3 @@ #!/usr/bin/env node
 import { peepholeModule } from "./peephole.js";
-import { emitLeanFile } from "./lean-emit.js";
+import { emitLeanFile, resetLeanModule } from "./lean-emit.js";
 import { emitDafnyFile } from "./dafny-emit.js";
@@ -265,2 +265,3 @@ import { dafnyGen, dafnyCheckDiff, dafnyVerify, dafnyRegen } from "./dafny-commands.js";
     defFile = peepholeModule(defFile, "lean");
+    resetLeanModule(); // clear per-module emitter state so batch mode doesn't leak into this module
     const typesPath = typesFile ? path.join(dir, `${leanBase}.types.lean`) : null;
@@ -267,0 +268,0 @@ const typesText = typesFile ? emitLeanFile(typesFile) : null;

New alerts

Long strings

Supply chain risk

Contains long string literals, which may be a sign of obfuscated or packed code.

Improved metrics

Total package byte prevSize

623634

0.28%

Lines of code

12203

0.27%

Worsened metrics

Number of low supply chain risk alerts

8

14.29%

No dependency changes