CLI reference (lsc)

The lsc command drives the whole toolchain. Install it globally (npm install -g lemmascript) or run it from a source checkout with npx tsx tools/src/lsc.ts.

lsc <gen|gen-check|check|regen|extract|info> [--backend=lean|dafny] [flags] <file.ts>
lsc config [--config=path] [<file.ts>]
lsc <gen|gen-check|check> [--backend=…] [--slow]        # no file: batch over LemmaScript-files.txt
lsc claimcheck [<file.ts>] [flags…]                     # forwards to lemmascript-claimcheck

All flags use the --flag=value form. Space-separated flags (--backend lean) and unknown flags are rejected with an error rather than silently ignored. Every command exits 0 on success and 1 on any failure.

Commands

Command	What it does
lsc gen <file.ts>	Generate backend code (next to the source unless proof-dir is configured)
lsc gen-check <file.ts>	gen, then verify the hand-edited file is additions-only vs. the generated one (Dafny)
lsc check <file.ts>	gen + additions-only check + run the prover — the full loop
lsc regen <file.ts>	Regenerate after a TS edit, three-way-merging to preserve proof additions (Dafny)
lsc extract <file.ts>	Dump the Raw IR as JSON to stdout (backend-neutral)
lsc info <file.ts>	Write <file>.ts.json, a per-function spec summary (backend-neutral)
lsc config [<file.ts>]	Show the discovered config, effective options, and resolved Dafny artifact directory
lsc claimcheck [<file.ts>]	Check each function’s plain-English //@ contract against its formal clauses

lsc gen

Generates backend files next to your TypeScript source unless a Dafny proof-dir is configured.

• Dafny (--backend=dafny, the default): writes <name>.dfy.gen (always regeneratable — never edit) and, on first run, <name>.dfy (the file you and your proofs own; starts as a copy of .dfy.gen).
• Lean (--backend=lean): writes <name>.types.lean (when the module declares types) and <name>.def.lean.

lsc check

The whole loop for one file: generate, confirm the diff between <name>.dfy and <name>.dfy.gen is additions-only, then run the prover (dafny verify, or lake build for Lean). Passes only when every contract holds.

lsc check --backend=dafny src/domain.ts
lsc check --backend=dafny --time-limit=120 src/domain.ts
lsc check --backend=dafny --extra-flags="--isolate-assertions" src/domain.ts

lsc regen

After editing the TypeScript, regenerate without losing proof work: the new generated code is three-way-merged into <name>.dfy (using <name>.dfy.base), preserving your helper lemmas, ghost predicates, and asserts, then re-verified.

Never delete <name>.dfy and gen fresh — you’d lose every proof addition. regen is the safe path. Use --no-verify to run only the merge and additions-only check, skipping the prover (CI uses this when a separate check pass does the verifying).

Recovery state depends on the failure stage. A conflict restores the original proof and retains the old .dfy.base; an additions-only failure also retains that anchor. If the merge is clean and additions-only but verification fails, .dfy.base instead advances to the new generation already present in the proof. Keep it while fixing the proof. A successful regen removes the anchor, also under --no-verify. Do not discard an anchor solely because a command failed.

lsc extract and lsc info

Backend-neutral: they run regardless of any //@ backend directive.

• extract prints the structured Raw IR as JSON — the supported way for external tools to consume LemmaScript’s frontend instead of re-parsing TypeScript.
• info writes <file>.ts.json: each function’s signature plus its requires / ensures / decreases clauses. Tools like lemmascript-seal build on this.

lsc config

Discovers the nearest lemmascript.json above a source file and prints its effective options after top-of-file overrides. With a file, the report also contains the absolute Dafny artifact directory; without one, discovery starts at the current directory. Use --config=<path> to pin a particular file.

{
  "extern-default": "impure",
  "safe-slice": true,
  "proof-dir": "proofs"
}

lsc claimcheck

Forwards to the bundled lemmascript-claimcheck CLI, which cross-examines the plain-English //@ contract line against the formal clauses. With a file, it checks that file (extra flags pass through verbatim); with no file, it runs once per entry in LemmaScript-files.txt.

Batch mode

Run gen, gen-check, or check with no file argument to batch over LemmaScript-files.txt in the current directory — one entry per line:

src/domain.ts
src/allocate.ts 120
src/scanner.ts 300 --isolate-assertions

Format: filepath [timeout_in_seconds] [extra prover flags…]. Batching is fail-fast — the first failing entry stops the run.

By default, a Dafny check batch runs gen-check (generation + additions-only, no proving) for entries whose manifest timeout exceeds 60 seconds. Pass --slow to verify those entries with their manifest timeouts, or supply --time-limit to verify every entry with that timeout, even above 60 seconds.

CLI --time-limit and --extra-flags values override the corresponding manifest values independently. Omitted options retain each entry’s setting; an explicit --extra-flags= clears its flags. Repeating either flag is an error.

lsc check --backend=dafny --time-limit=120  # verify every entry with this limit
lsc check --backend=dafny --extra-flags="--isolate-assertions"

Flags

Flag	Applies to	Meaning
--backend=dafny|lean	all except extract/info	Backend to target. Default: dafny
--config=<path>	config-aware commands	Pin lemmascript.json instead of nearest-ancestor discovery
--time-limit=<seconds>	check, regen	Prover time limit (positive integer)
--extra-flags="…"	check, regen	Extra flags passed to the prover verbatim
--slow	batch check	Verify long-timeout entries instead of downgrading them
--no-verify	regen	Merge + additions-only check only; skip the prover

In-file directives the CLI honors

Directive	Effect
//@ backend <dafny|lean>	The file belongs to one backend; commands for the other backend skip it (extract/info always run)
//@ option <key> <value>	Override an eligible project option before the first source statement
//@ safe-slice	Legacy alias for //@ option safe-slice true
//@ lean-module <name>	Overrides the Lean module base name (Lean module names are global; this prevents collisions between identically-named files)

Project resolution

lsc resolves imports using the nearest tsconfig.json and options using the nearest lemmascript.json above the source file. Without a TS config it falls back to strict ESNext defaults; without a LemmaScript config it uses backward- compatible option defaults. From a source checkout, the equivalent of lsc is npx tsx <checkout>/tools/src/lsc.ts — no build step needed.

For Lean checks, the nearest ancestor containing either lakefile.lean or lakefile.toml is the build directory. Discovery starts in the source directory and includes the filesystem root. A nearer TOML project takes precedence over an outer Lean project, and vice versa. If neither file is found, lsc check reports an error without starting Lake. A missing proof file also fails before Lake is started.

Next

• Installation — get lsc on your PATH
• Supported TypeScript subset — what the toolchain can express
• Full specification — precise semantics of the annotation language