openmath-rocq-theorem

Configures Rocq environments, runs preflight checks, and guides the proving workflow for OpenMath Rocq theorems. Use when the user wants to set up Rocq tooli...

Security Scan

The skill's instructions, requirements, and files are internally consistent with a helper for setting up and running Rocq/Coq proofs and do not request unrelated credentials or perform unexpected installation steps.

Purpose & Capability

Name/description match the requested actions: the skill guides Rocq/Coq proving, checks for rocq/coqc, dune, and opam, and references companion skills. No unrelated binaries, credentials, or config paths are asked for.

Instruction Scope

SKILL.md instructs only local workspace commands (rocq, dune, opam, grep, etc.), preflight checks, and a proof loop. It does not instruct reading unrelated system files, exfiltrating data, or calling external endpoints. It does assume a previously created theorem workspace and references only local project files.

Install Mechanism

No install spec and no bundled code — instruction-only. Nothing is downloaded or written to disk by the skill itself, minimizing install-time risk.

Credentials

The skill requires no environment variables, credentials, or config paths. The declared runtime commands (rocq, dune, opam) are appropriate for the stated purpose.

Persistence & Privilege

always is false and the skill is user-invocable. It does not request persistent presence or modify other skills/configs. Autonomous invocation remains allowed by platform default but is not a special privilege here.

Assessment

This package is coherent for helping with Rocq/Coq proofs. Before running its suggested commands, run them in a project-local or isolated environment (container/VM) for untrusted code. Be cautious when running opam install on unreviewed projects (build/install hooks can execute code). If you rely on companion skills, install them only after reviewing their source or installing them into a deliberate local skills directory.

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 (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, rocq-setup, or rocq-dune are 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-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.

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), 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.
• Install boundary: This isolated skill should not instruct copying unseen 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.
• Stdlib prefix: Use 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.
• Verification status: A proof is complete only when dune build exits 0, no admit or Admitted. 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.