Run log: record check and regen runs

AGENTS.md

@@ -23,6 +23,8 @@ Default backend is Dafny. Pass `--backend=...` explicitly anyway — case-study
 
 If `lemmascript.json` sets `proof-dir`, all Dafny companions (`.dfy.gen`, `.dfy`, `.dfy.base`, `.dfy.merged`) live in the mirrored directory reported by `lsc config`, not beside the TS file. The edit boundaries and regen rules below apply at that mapped location unchanged.
 
+`lsc check` and `lsc regen` record each Dafny run in `.lemmascript/` (self-ignored by git; see SPEC.md §7.7). Leave it alone — it is the record of what verification caught. `LSC_RUN_LOG=false` turns it off for one run.
+
 After editing `lsc` itself (anything under `tools/`), run `npm run build` before re-invoking `npx lsc` — the CLI runs the compiled `tools/dist/lsc.js`, not the TS source.
 
 ## File-edit boundaries

SPEC.md

@@ -1334,6 +1334,8 @@ Default backend is Dafny. `extract` and `info` are backend-neutral and always ru
 - `--extra-flags=<string>` — extra flags forwarded verbatim to the backend prover.
 - `--slow` — in batch mode, verify entries whose manifest timeout exceeds 60s (otherwise those get `gen-check`, unless `--time-limit` is supplied).
 
+**Environment:** `LSC_RUN_LOG=false` turns the run log (§7.7) off for one invocation; `true` or unset leaves it to `run-log` in `lemmascript.json`. Any other value is an error. It is the only environment variable `lsc` reads.
+
 In batch mode, `--time-limit` and `--extra-flags` independently override the
 corresponding manifest values; omitted options retain the per-entry settings.
 For Dafny `check`, an explicit timeout enables verification even above 60s without `--slow`.
@@ -1347,11 +1349,11 @@ For Dafny `check`, an explicit timeout enables verification even above 60s witho
 ### 7.2 `check`
 
 - **Lean:** gen + `lake build` (checks `.def.lean` + `.proof.lean` + `.spec.lean`)
-- **Dafny:** gen + additions-only check + `dafny verify`
+- **Dafny:** gen + additions-only check + `dafny verify`; the run is recorded in the run log (§7.7)
 
 ### 7.3 `regen` (Dafny only)
 
-Three-way merge when generated code changes. See [SPEC_DAFNY.md](SPEC_DAFNY.md).
+Three-way merge when generated code changes. See [SPEC_DAFNY.md](SPEC_DAFNY.md). Each run, including a conflict or additions-only failure, is recorded in the run log (§7.7).
 
 ### 7.4 `info`
 
@@ -1392,6 +1394,7 @@ it; absent means current behavior. Unknown keys and bad values are errors.
 | `proof-dir` | relative path | source directory | no (Dafny only) |
 | `string-semantics` | `unicode-scalar` \| `javascript-utf16` | `unicode-scalar` | yes (Dafny only) |
 | `dafny-library` | `stdlib` \| `local` | `stdlib` | yes (Dafny only) |
+| `run-log` | boolean | `true` | no (Dafny only) |
 
 Eligible settings use `//@ option <key> <value>` before the first source
 statement. File values override project values; duplicates are errors.
@@ -1423,6 +1426,22 @@ See [examples/utf16.ts](examples/utf16.ts) and its Dafny proof. Compatibility is
 after project values and file directives are merged. Collection libraries may differ
 between files; unlike the string model, they do not change the meaning of contracts.
 
+### 7.7 Run log
+
+Every Dafny `check` and `regen` appends one JSON record to `.lemmascript/runs.jsonl`, in the
+directory of the selected `lemmascript.json` (else the source's git root, else the current
+directory), and stores the source as `.lemmascript/blobs/<hash>.ts`. The directory contains a
+`.gitignore` of `*`, so it never appears in `git status`. A record names the file, the command,
+the stage where the run stopped (`ok`, `verify`, `resolve`, `diff`, `conflict`), the members that
+passed and failed, hashes of the `.ts` and `.dfy`, and `partial: true` when the run did not
+report on every member. Logging never changes `lsc` output or exit codes.
+
+```json
+{ "run-log": false }
+```
+
+turns it off for a project; `LSC_RUN_LOG=false` turns it off for one run.
+
 ---
 
 ## 8. Pipeline

TOOLS.md

@@ -172,6 +172,8 @@ not implement routing themselves.
 - `lsc regen --backend=dafny foo.ts` — regenerate `.dfy.gen`, three-way merge, verify
 - `lsc check --backend=dafny foo.ts` — gen + additions-only check + `dafny verify`
 
+`check` and `regen` pass an optional `RunLog` (`run-log.ts`) to these helpers, and each records the stage it detects: `dafnyCheckDiff` records `diff`, `dafnyVerify` records `ok`/`verify`/`resolve`, and `dafnyRegen` records `conflict` and `--no-verify` runs. Recording lives in the helpers only because they end runs with `process.exit`; if they ever return outcomes instead, it belongs in `lsc.ts`. Dafny keeps inherited stdio; member outcomes come from `--log-format text` written to a temp file.
+
 ## Narrow Rules
 
 `narrow.ts` (structural-narrowing rewrite pass) takes typed IR and rewrites narrowing patterns into IR nodes that transform lowers uniformly: `someMatch` (binary, for optional checks) or `tagMatch` (multi-case, for discriminated unions). Each carries the scrutinee, the matched cases, and the fallthrough.
@@ -304,4 +306,5 @@ The Dafny emitter wraps `if-then-else` and `let` (var-binding) expressions in pa
 | `dafny-commands.ts` | CLI | Dafny gen/gen-check/regen/check commands |
 | `info-command.ts` | CLI | `lsc info` — per-function spec summary JSON; `--typed` — Typed IR contract for satellites |
 | `config.ts` | CLI/shared | Option registry, config discovery/validation, file overrides, artifact path mapping |
+| `run-log.ts` | CLI | Run log: `.lemmascript/` directory, source snapshots, one record per Dafny `check`/`regen` |
 | `lsc.ts` | CLI | Wires the pipeline, dispatches to backend |

site/src/content/docs/reference/cli.md

@@ -97,14 +97,22 @@ at the current directory. Use `--config=<path>` to pin a particular file.
   "string-semantics": "unicode-scalar",
   "dafny-library": "stdlib",
   "safe-slice": true,
-  "proof-dir": "proofs"
+  "proof-dir": "proofs",
+  "run-log": true
 }
 ```
 
 `dafny-library` selects `stdlib` (default) or generated `local` helpers for collection
 operations. Enabling `"string-semantics": "javascript-utf16"` requires explicitly setting
 `"dafny-library": "local"`; an omitted or explicit `stdlib` choice is an error.
 
+`run-log` (default `true`) records every Dafny `check` and `regen` in `.lemmascript/`
+beside `lemmascript.json` (without one, at the git repository root, or else in the current
+directory): one line per run in `runs.jsonl` (the stage it stopped at and
+which members passed or failed) plus a snapshot of the source. The directory ignores
+itself in git, and logging never changes `lsc` output or exit codes. Set it to `false` to
+turn logging off for the project, or `LSC_RUN_LOG=false` for a single run.
+
 A file can override both project settings before its first statement:
 
 ```typescript

tools/src/config.ts

@@ -45,6 +45,12 @@ export const OPTION_SPECS = {
     fileOverride: true,
     description: "Use Dafny's standard library or generated local helpers for collection operations.",
   },
+  "run-log": {
+    type: "boolean",
+    default: true,
+    fileOverride: false,
+    description: "Record lsc check and regen runs in .lemmascript/.",
+  },
 } as const;
 
 type OptionSpecs = typeof OPTION_SPECS;

tools/src/dafny-commands.ts

@@ -6,6 +6,7 @@ import { existsSync, readFileSync, writeFileSync, copyFileSync, unlinkSync } fro
 import { execFileSync } from "child_process";
 import path from "path";
 import { DEFAULT_OPTIONS, parseOptionValue, type LscOptions } from "./config.js";
+import type { RunLog } from "./run-log.js";
 
 function writeGen(genPath: string, text: string) {
   writeFileSync(genPath, text);
@@ -20,7 +21,13 @@ export function dafnyGen(genPath: string, dfyPath: string, text: string) {
   }
 }
 
-export function dafnyCheckDiff(genPath: string, dfyPath: string): boolean {
+export function dafnyCheckDiff(genPath: string, dfyPath: string, log?: RunLog): boolean {
+  const ok = additionsOnly(genPath, dfyPath);
+  if (!ok) log?.finish({ stage: "diff", exit: 1, dfyPath });
+  return ok;
+}
+
+function additionsOnly(genPath: string, dfyPath: string): boolean {
   for (const filePath of [genPath, dfyPath]) {
     if (!existsSync(filePath)) {
       console.error(`ERROR: cannot verify additions-only diff; file does not exist: ${filePath}`);
@@ -134,23 +141,34 @@ export function dafnyVerifyArgs(content: string, timeLimit?: number, extraFlags?
   return { args };
 }
 
-export function dafnyVerify(dfyPath: string, dir: string, timeLimit?: number, extraFlags?: string): boolean {
+export function dafnyVerify(dfyPath: string, dir: string, timeLimit?: number, extraFlags?: string, log?: RunLog): boolean {
   console.log("Running dafny verify...");
   try {
     const { args, error } = dafnyVerifyArgs(readFileSync(dfyPath, "utf-8"), timeLimit, extraFlags);
-    if (error) { console.error(error); return false; }
+    if (error) {
+      console.error(error);
+      log?.finish({ stage: "resolve", exit: 1, dfyPath });
+      return false;
+    }
+    if (log) args.push(...log.dafnyArgs());
     args.push(dfyPath);
     execFileSync("dafny", args, { cwd: dir, stdio: "inherit" });
+    log?.finish({ stage: "ok", exit: 0, dfyPath, results: log.readResults() });
     return true;
   } catch (e: any) {
     if (e?.code === "ENOENT") {
       console.error("ERROR: `dafny` not found on PATH — verification never ran. Install Dafny 4.x: https://dafny.org/");
+      log?.discard();
+      return false;
     }
+    // Dafny writes no results when it stops at parsing or resolution.
+    const results = log?.readResults() ?? null;
+    log?.finish({ stage: results ? "verify" : "resolve", exit: 1, dfyPath, results });
     return false;
   }
 }
 
-export function dafnyRegen(genPath: string, dfyPath: string, basePath: string, text: string, dir: string, timeLimit?: number, extraFlags?: string, noVerify = false) {
+export function dafnyRegen(genPath: string, dfyPath: string, basePath: string, text: string, dir: string, timeLimit?: number, extraFlags?: string, noVerify = false, log?: RunLog) {
   // 1. Read old gen before overwriting (needed for base seeding)
   const oldGen = existsSync(genPath) ? readFileSync(genPath, "utf-8") : "";
 
@@ -161,10 +179,11 @@ export function dafnyRegen(genPath: string, dfyPath: string, basePath: string, t
   if (!existsSync(dfyPath)) {
     writeFileSync(dfyPath, text);
     console.log(`Created: ${path.basename(dfyPath)}`);
-    if (!noVerify && !dafnyVerify(dfyPath, dir, timeLimit, extraFlags)) {
+    if (!noVerify && !dafnyVerify(dfyPath, dir, timeLimit, extraFlags, log)) {
       console.error(`FAILED: ${path.basename(dfyPath)} verification failed on first run.`);
       process.exit(1);
     }
+    log?.finish({ stage: "ok", exit: 0, dfyPath });
     return;
   }
 
@@ -185,20 +204,21 @@ export function dafnyRegen(genPath: string, dfyPath: string, basePath: string, t
         copyFileSync(dfyPath, mergedPath);
         writeFileSync(dfyPath, savedDfy);
         console.error(`CONFLICT: ${path.basename(dfyPath)} — merge had conflicts, dfy restored. See ${path.basename(mergedPath)}`);
+        log?.finish({ stage: "conflict", exit: 1, dfyPath });
         process.exit(1);
       }
       throw e;
     }
   }
 
   // 6. Check gen invariant (unconditional)
-  if (!dafnyCheckDiff(genPath, dfyPath)) {
+  if (!dafnyCheckDiff(genPath, dfyPath, log)) {
     console.error(`FAILED: ${path.basename(dfyPath)} has modifications to generated lines.`);
     process.exit(1);
   }
 
   // 7. Verify (skipped under --no-verify: caller verifies separately)
-  if (!noVerify && !dafnyVerify(dfyPath, dir, timeLimit, extraFlags)) {
+  if (!noVerify && !dafnyVerify(dfyPath, dir, timeLimit, extraFlags, log)) {
     // The clean merge already incorporated this generation into the proof
     // file. Keep that generation as the next merge anchor even though the
     // verifier rejected the current proof state; otherwise the next regen
@@ -208,6 +228,8 @@ export function dafnyRegen(genPath: string, dfyPath: string, basePath: string, t
     process.exit(1);
   }
 
-  // 8. Success — delete base (gen is now the anchor)
+  // 8. Success — delete base (gen is now the anchor). After a verified run
+  // dafnyVerify has already recorded the outcome; this records --no-verify.
   if (existsSync(basePath)) unlinkSync(basePath);
+  log?.finish({ stage: "ok", exit: 0, dfyPath });
 }

tools/src/lsc.ts

@@ -21,6 +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 {
   findUp,
   loadConfigOptions,
@@ -337,6 +338,8 @@ function runFile(
 
   const fullText = sourceFile.getFullText();
   const { options, configFile } = effectiveOptions(absPath, fullText, configPath);
+  // Checked here, for every command, so a bad LSC_RUN_LOG fails like a bad config value.
+  const runLogOn = runLogEnabled(options["run-log"], process.env.LSC_RUN_LOG);
 
   // Check //@ backend directive — skip if backend doesn't match.
   // `extract` and `info` are backend-neutral and always run.
@@ -420,6 +423,13 @@ function runFile(
     guardRelocatedDafnyProof(dir, artifactDir, base, dfyPath);
     mkdirSync(artifactDir, { recursive: true });
 
+    // Record check/regen runs in the run log. Created after the proof-dir guard
+    // 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() })
+      : undefined;
+
     if (cmd === "gen") { dafnyGen(genPath, dfyPath, text); return; }
     if (cmd === "gen-check") {
       dafnyGen(genPath, dfyPath, text);
@@ -428,11 +438,11 @@ function runFile(
     }
     if (cmd === "check") {
       dafnyGen(genPath, dfyPath, text);
-      if (!dafnyCheckDiff(genPath, dfyPath)) process.exit(1);
-      if (!dafnyVerify(dfyPath, artifactDir, timeLimit, extraFlags)) process.exit(1);
+      if (!dafnyCheckDiff(genPath, dfyPath, log)) process.exit(1);
+      if (!dafnyVerify(dfyPath, artifactDir, timeLimit, extraFlags, log)) process.exit(1);
       return;
     }
-    if (cmd === "regen") { dafnyRegen(genPath, dfyPath, basePath, text, artifactDir, timeLimit, extraFlags, noVerify); return; }
+    if (cmd === "regen") { dafnyRegen(genPath, dfyPath, basePath, text, artifactDir, timeLimit, extraFlags, noVerify, log); return; }
     console.error(`Unknown command: ${cmd}`);
     process.exit(1);
   }