fix: keep an unreadable version from failing a logged run

DESIGN_RUN_LOG.md

@@ -71,7 +71,7 @@ The helper that detects how the run ended appends one record: `dafnyCheckDiff` f
 - **`stage`** tells where the run stopped. `diff` means the additions-only check failed, so Dafny never ran. `resolve` means Dafny wrote no member results (a parse or resolution error, or `lsc` refused the proof before running Dafny). If Dafny is not installed, nothing was verified and the run is not recorded. `conflict` means a `regen` merge conflicted. `verify` means Dafny ran and reported failures. `ok` means everything that ran passed.
 - **`failed` / `passed`** are member names. A member that fails either check appears once, in `failed`.
 - **`partial`** is `true` when the run did not report on every member: Dafny never ran or wrote no results, `regen --no-verify`, or a `--filter-symbol` / `--filter-position` flag. Only a non-partial run can make a member disappear (§4).
-- **`exit`** is the exit code `lsc` ends with. **`v`** is the record schema version; **`id`** is a random UUID; `lsc` (the version) gives context; fields such as the git commit or whether the run came from CI can be added in a later schema version if records leave the machine.
+- **`exit`** is the exit code `lsc` ends with. **`v`** is the record schema version; **`id`** is a random UUID; `lsc` (the version, or `null` when it can't be read) gives context; fields such as the git commit or whether the run came from CI can be added in a later schema version if records leave the machine.
 - **`tsHash` / `dfyHash`** are the first 12 hex characters of the SHA-256 of the source `.ts` and of the proof `.dfy`. The `.ts` is hashed when the run starts. The `.dfy` is hashed when the run ends, because `check` may create it and `regen` may merge into it.
 
 **Snapshots.** On every run, `lsc` copies the `.ts` to `.lemmascript/blobs/<tsHash>.ts` unless that file already exists. Most runs during proof work leave the `.ts` unchanged, so they add nothing. The `.dfy` is not snapshotted, because labeling only needs to see what changed in the program and its spec.

tools/src/lsc.ts

@@ -21,7 +21,7 @@ import { emitDafnyFile, emittedNameMap } from "./dafny-emit.js";
 import { dafnyGen, dafnyCheckDiff, dafnyVerify, dafnyRegen } from "./dafny-commands.js";
 import { leanGen, leanCheck } from "./lean-commands.js";
 import { runInfo, runTypedInfo, type TypedInfoDafny } from "./info-command.js";
-import { RunLog, resolveLogDir, runLogEnabled } from "./run-log.js";
+import { RunLog, resolveLogDir, runLogEnabled, safely } from "./run-log.js";
 import { runRuns } from "./runs-command.js";
 import {
   findUp,
@@ -436,7 +436,7 @@ function runFile(
     // so an aborted run leaves no snapshot; each helper records the stage it detects.
     const logCmd = cmd === "check" || cmd === "regen" ? cmd : null;
     const log = logCmd && runLogOn
-      ? new RunLog({ logDir: resolveLogDir(absPath, configFile), cmd: logCmd, sourcePath: absPath, extraFlags, lscVersion: lscVersion() })
+      ? new RunLog({ logDir: resolveLogDir(absPath, configFile), cmd: logCmd, sourcePath: absPath, extraFlags, lscVersion: safely(lscVersion) })
       : undefined;
 
     if (cmd === "gen") { dafnyGen(genPath, dfyPath, text); return; }

tools/src/run-log.ts

@@ -42,15 +42,15 @@ export interface VerifyRecord {
   passed: string[];
   tsHash: string | null;
   dfyHash: string | null;
-  lsc: string;
+  lsc: string | null;
 }
 
 export interface RunLogInit {
   logDir: string;
   cmd: "check" | "regen";
   sourcePath: string;
   extraFlags?: string;
-  lscVersion: string;
+  lscVersion: string | null;
 }
 
 /**
@@ -115,7 +115,7 @@ export function hashText(text: string): string {
   return createHash("sha256").update(text).digest("hex").slice(0, 12);
 }
 
-function safely<T>(fn: () => T): T | null {
+export function safely<T>(fn: () => T): T | null {
   try {
     return fn();
   } catch {

tools/tests/run-log.test.ts

@@ -8,7 +8,7 @@ import { tmpdir } from "node:os";
 import { delimiter, join } from "node:path";
 import { dafnyCheckDiff, dafnyRegen, dafnyVerify } from "../src/dafny-commands.ts";
 import {
-  RunLog, ensureLogDir, hashText, isPartialRun, parseTextLog, readRecords, resolveLogDir, runLogEnabled, snapshotSource,
+  RunLog, ensureLogDir, hashText, isPartialRun, parseTextLog, readRecords, resolveLogDir, runLogEnabled, safely, snapshotSource,
 } from "../src/run-log.ts";
 
 const posixOnly = { skip: process.platform === "win32" };
@@ -328,6 +328,19 @@ test("an unwritable log directory never throws", () => {
   }
 });
 
+test("a version that can't be read is recorded as null", () => {
+  const root = tempDir();
+  try {
+    const source = join(root, "a.ts");
+    writeFileSync(source, "");
+    const lscVersion = safely((): string => { throw new Error("ENOENT: no such file or directory, open 'package.json'"); });
+    new RunLog({ logDir: root, cmd: "check", sourcePath: source, lscVersion }).finish({ stage: "ok", exit: 0, dfyPath: source });
+    assert.equal(records(root)[0].lsc, null);
+  } finally {
+    rmSync(root, { recursive: true, force: true });
+  }
+});
+
 test("dafnyArgs points Dafny at a temporary text log that readResults parses", () => {
   const root = tempDir();
   try {