npx claudepluginhub llm4rocq/rocq-skills --plugin rocq# Rocq Checkpoint Creates a checkpoint with per-file and project-wide build verification, axiom check, and commit. ## Usage ## Inputs | Arg | Required | Description | |-----|----------|-------------| | message | No | Custom commit message suffix | ## Actions 1. **Verify Touched Files** - For each existing added/modified `.v` file in the staged set, compile individually via `rocq_compile(source)` or `coqc`: If any file fails, stop and report the error before proceeding. 2. **Verify Build** - Run project-wide build gate: 3. **Check Axioms** - Verify no unwanted custom axiom...
/checkpointCreates or verifies git checkpoints logging state and comparing changes, tests passed, coverage, build status. Also supports list and clear subcommands.
/checkpointCreates or verifies git checkpoints logging state and comparing changes, tests passed, coverage, build status. Also supports list and clear subcommands.
/checkpointSaves a Markdown checkpoint capturing session progress, git state, open questions, and prioritized next steps to .claude/checkpoints/<timestamp>.md. Updates CLAUDE.md and commits changes.
/checkpointSaves or restores git working directory checkpoints capturing staged/unstaged changes and untracked files. Supports list, diff, delete subcommands with optional --tag.
/checkpointVerifies Lean4 file compilations, project build, axioms, and sorries, then commits touched files as a safe checkpoint. Optional custom message.
/checkpointStages relevant changes, creates a descriptive git commit, and writes .claude/handoff.md with progress summary, pending tasks, and learnings.
Creates a checkpoint with per-file and project-wide build verification, axiom check, and commit.
/rocq:checkpoint
/rocq:checkpoint "optional custom message"
| Arg | Required | Description |
|---|---|---|
| message | No | Custom commit message suffix |
.v file in the staged set, compile individually via rocq_compile(source) or coqc:
coqc -Q . ProjectName <path/to/File.v> # or use rocq_compile
make -f CoqMakefile # or coq_makefile generated Makefile
bash "$ROCQ_SCRIPTS/check_axioms.sh" .
rocq_query("Print Assumptions theorem_name.") for each theorem.${ROCQ_PYTHON_BIN:-python3} "$ROCQ_SCRIPTS/admitted_analyzer.py" . --format=summary
git add <files touched during this session>
git diff --cached --name-only # print exact staged set
git commit -m "checkpoint(rocq): [summary]"
git add -A or broad glob patterns.## Checkpoint Created
**Commit:** [hash] - [message]
**Touched files compiled:** N files
**Project build:** passing
**Admitted:** [N] remaining
**Axioms:** [status]
**Next steps:**
- Continue with `/rocq:prove`
- Push manually when ready: `git push`
git reset --soft HEAD~1 # Undo last, keep staged
git reset HEAD~1 # Undo last, keep unstaged
git reset HEAD~N # Undo last N commits
Warning: Only use reset before pushing.
/rocq:prove - Guided cycle-by-cycle proving/rocq:review - Read-only code review/rocq:refactor - Strategy-level proof simplification