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.
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.
Environment: Verify rocq (or coqc), dune, and opam are installed and the active opam switch matches the project's .opam-switch or opam file. See the rocq-setup skill for installation and switch management.
Companion skills: If companion Rocq skills such as rocq-proof, rocq-ssreflect, , or are already installed in the active agent, use them. See for when each one is useful. This isolated package does not include their code and does not install them for you.
rocq-setuprocq-dunePreflight: 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-proof or rocq-ssreflect is already installed, use them as companion guidance; otherwise continue with the local workflow in this skill.
Verify: Confirm dune build (or rocq compile <file>.v) passes and no admit or Admitted. remains:
dune build
grep -rn 'admit\|Admitted\.' *.v
Submit: Use the openmath-submit-theorem skill to hash and submit the proof.
| 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. |
rocq-proof (proving methodology, tactic reference, Ltac2), rocq-ssreflect (SSReflect / MathComp style), rocq-setup (opam, toolchain, editor), and rocq-dune (build system, _CoqProject, dune stanzas) are useful companions when already installed. Optional companions: rocq-mwe, rocq-bisect, rocq-extraction, rocq-mathcomp-build.rocq-* directories into ~/.agents/skills or 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/skills or .claude/skills.From Stdlib Require Import for Rocq 9.x. The legacy From Coq Require Import still works with a deprecation warning; prefer From Stdlib for all new proofs.dune build exits 0, no admit or Admitted. remains, and the LSP panel shows no errors or warnings.Load when needed (one level from this file):