ClawHub

openmath-rocq-theorem

v1.0.3

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...

⭐ 0· 83·1 current·1 all-time
byshentu-org@bennyzhe·duplicate of @bennyzhe/openmath-lean-theorem (1.0.2)
MIT-0
Download zip
LicenseMIT-0 · Free to use, modify, and redistribute. No attribution required.
Security Scan
VirusTotalVirusTotal
Benign
View report →
OpenClawOpenClaw
Benign
high confidence
✓
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.

Like a lobster shell, security has layers — review code before you run it.

latestvk97ay02e2kqnb3m3c0j13ed3b983j8ne

License

MIT-0
Free to use, modify, and redistribute. No attribution required.
Termshttps://spdx.org/licenses/MIT-0.html

Comments