- name
- openmath-rocq-theorem
- description
- Configures Rocq environments, runs preflight checks, and guides the proving workflow for OpenMath Rocq theorems. Use when the user wants to set up Rocq tooling, prove a downloaded OpenMath theorem in Rocq/Coq, or verify and submit a Rocq proof.
- version
- v1.0.2
- requirements
- commands
- side_effects
OpenMath Rocq Theorem
Instructions
Set up the Rocq proving environment, validate opam switches, and prove downloaded OpenMath theorems. Assumes the theorem workspace was already created by the openmath-open-theorem skill.
This skill package is self-contained: it consists of this SKILL.md plus the local references/ files in this directory. It does not bundle or install sibling rocq-* companion skills.
Workflow checklist
- [ ] Environment: Verify
rocq(orcoqc),dune, andopamare installed and the active opam switch matches the project's.opam-switchoropamfile. See therocq-setupskill for installation and switch management. - [ ] Companion skills: If companion Rocq skills such as
rocq-proof,rocq-ssreflect,rocq-setup, orrocq-duneare already installed in the active agent, use them. See references/companions.md for when each one is useful. This isolated package does not include their code and does not install them for you. - [ ] Preflight: Confirm the environment is healthy before proving:
rocq --version
rocq -e 'From Stdlib Require Import Arith. Check Nat.add_comm.'
dune --version
opam list rocq-prover- [ ] Prove: Follow the minimal Rocq proving loop in references/proof_playbook.md. If
rocq-prooforrocq-ssreflectis already installed, use them as companion guidance; otherwise continue with the local workflow in this skill. - [ ] Verify: Confirm
dune build(orrocq compile <file>.v) passes and noadmitorAdmitted.remains:
dune build
grep -rn 'admit\|Admitted\.' *.v- [ ] Submit: Use the
openmath-submit-theoremskill to hash and submit the proof.
Scripts
| Action | Command | Use when | |
|---|---|---|---|
| Check Rocq version | rocq --version | Verify the active opam switch has the expected Rocq release. | |
| Verify stdlib loads | rocq -e 'From Stdlib Require Import Arith. Check Nat.add_comm.' | Confirm the standard library is reachable before proving. | |
| Build project | dune build | After each proof attempt; must exit 0 with no errors. | |
| Compile single file | rocq compile <file>.v | Quick check on a single .v file without a full dune build. | |
| Check for admits | `grep -rn 'admit\ | Admitted\.' *.v` | Before submitting; must return no matches. |
| Install opam deps | opam install . --deps-only | After cloning or changing the project opam file. |
Notes
- Rocq version: OpenMath Rocq workspaces target Rocq 9.1.0 (current stable, September 2025) with Platform 2025.08.2.
- Companion skills:
rocq-proof(proving methodology, tactic reference, Ltac2),rocq-ssreflect(SSReflect / MathComp style),rocq-setup(opam, toolchain, editor), androcq-dune(build system,_CoqProject, dune stanzas) are useful companions when already installed. Optional companions:rocq-mwe,rocq-bisect,rocq-extraction,rocq-mathcomp-build. - Install boundary: This isolated skill should not instruct copying unseen
rocq-*directories into~/.agents/skillsor any other global skills directory. If you are installing from the full repository, review the companion skill folders there and copy them only into a deliberate project-local skills directory such as.codex/skillsor.claude/skills. - Stdlib prefix: Use
From Stdlib Require Importfor Rocq 9.x. The legacyFrom Coq Require Importstill works with a deprecation warning; preferFrom Stdlibfor all new proofs. - Verification status: A proof is complete only when
dune buildexits 0, noadmitorAdmitted.remains, and the LSP panel shows no errors or warnings.
References
Load when needed (one level from this file):
- references/companions.md — When to use optional Rocq companion skills if they are already installed.
- references/languages.md — Rocq version, Stdlib prefix, libraries, and proof style.
- references/proof_playbook.md — Minimal standalone proving loop for downloaded OpenMath Rocq theorem workspaces.