/checkpoint

name: checkpoint
description: Save progress with a safe commit checkpoint
user_invocable: true

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](../skills/lean4/references/command-invocation.md).

**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](../skills/lean4/references/command-invocation.md#validated-invocation-block-host-provided).

**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](#generated-root-files-gate) 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

Generated Root Files gate

Mathlib's generated root-import aggregators (`Mathlib.lean`, `Mathlib/Tactic.lean`, …) go stale when a `.lean` file is added, renamed, or deleted, and mathlib CI runs `lake exe mk_all --check` as a dedicated gate. This step catches that follow-up **before** the main build — but only when the current work is plausibly aimed at upstream mathlib contribution, so a personal mathlib fork used for experimentation is not blocked on every checkpoint.

**1. Resolve whether the gate fires and acquire the project root** (a flag resolving to true wins the *intent* decision; explicit false behaves like omission):

• `--no-mathlib-mk-all` true → gate skipped; done. No helper is consulted and no root is needed.
• Otherwise run `lean4-skills-project-context --from "$PWD"` to acquire **and** validate the project root, and validate the full record exactly as `/lean4:draft` does: `schema` = `project-context/v1`, `intent.contributing_upstream` a string in `yes | no | unknown`, `intent.source` a string in its domain — any missing/non-string/out-of-domain value is malformed helper output. Take `$project_root` from the record's non-null top-level `root`. Then:
• **`--mathlib-mk-all` true** → gate fires. The flag overrides only the *intent* decision, **not** root discovery: if project-context fails, is malformed, or returns a null `root`, **stop** (explicit opt-in must not fail open) — do not skip and do not proceed to the build.
• **no flag** → use `intent.contributing_upstream`: `yes` → gate fires; `no`, `unknown`, or a malformed/failed helper (including a null `root`) → gate skipped. Inferred intent may fail open (skip).

`mk_all_declared` is **never** consulted; availability is decided by actually running the command.

**2. Detect root-affecting candidate changes.** The **candidate set** is the session-touched files the *