checkpoint

Lean4 Checkpoint

Creates a checkpoint with per-file and project-wide build verification, axiom check, and commit.

Usage

/lean4:checkpoint
/lean4:checkpoint "optional custom message"
/lean4:checkpoint --mathlib-mk-all      # force the mk_all root-file gate
/lean4:checkpoint --no-mathlib-mk-all   # skip the mk_all root-file gate

Invocation Contract

Interpret this command's inputs per the Command Invocation Contract.

Primary path (hook-validated): If a validated-invocation block for this command appears in context, treat it as the authoritative interpretation of parser-decidable inputs and do not re-parse the raw invocation text for those inputs. Start by reading all parser-decided fields from the block. Emit the final Resolved Inputs summary from the block values. See Validated Invocation Block.

Fallback path (other hosts): If no validated-invocation block is present, parse the raw invocation text against this command's input table before acting.

Startup requirements:

1. Emit a Resolved Inputs block with explicit values, defaults, ignored flags, and startup validation errors — including the effective mk_all-gate decision and its source (flag, the helper's intent.source, or helper-failure).
2. Refuse to start on startup validation errors (e.g. both --mathlib-mk-all and --no-mathlib-mk-all).

Inputs

Arg	Required	Description
message	No	Custom commit message suffix
--mathlib-mk-all	No	Force the Generated Root Files gate on, overriding project-context detection. Mutually exclusive with --no-mathlib-mk-all.
--no-mathlib-mk-all	No	Force the Generated Root Files gate off, overriding project-context detection. Mutually exclusive with --mathlib-mk-all.

Actions

1. Verify Touched Files - For each existing added/modified .lean file in the candidate set for this checkpoint — the files touched during this session that the Stage and Commit step will stage, determined independently of the current git index (staging happens later) — compile individually:

   lake env lean <path/to/File.lean>   # from project root
   

   If any file fails, stop and report the error before proceeding.
2. Generated Root Files gate (mathlib) - See Generated Root Files below. Runs before the project build; skips entirely unless the gate fires.
3. Verify Build - Run lake build for the project-wide gate (catches cross-file issues not visible in per-file compilation)
4. Best-effort Axiom Scan - Scan for non-standard axioms in top-level declarations:

   lean4-skills-check-axioms-inline .
   

   Note: checks top-level unindented declarations across all namespaces in each file (nested, sibling, and dotted namespaces are tracked correctly; sections are handled without leaking into the qualified name). Recognizes theorem|lemma|def|instance|abbrev|example|structure|class|inductive|axiom|constant, optionally prefixed by noncomputable, unsafe, partial, or nonrec. Indented declarations and unicode-identifier decls are not matched — files whose decls all fall in those classes are surfaced as UNVERIFIED (exit 1, not a silent pass). The script temporarily edits files in place while running — only use on version-controlled files, and avoid concurrent editors or watchers.
5. Count Sorries - Report current sorry count:

   lean4-skills-sorry-analyzer . --format=summary
   

6. Stage and Commit - Stage only files touched during this session, then commit:

   git add <files touched during this session>
   git diff --cached --name-only   # print exact staged set
   git commit -m "checkpoint(lean4): [summary]"
   

   Never use git add -A or broad glob patterns.
7. Report Status - Show what was saved