Borrowing it
Nothing to install: this file belongs to plclub/hs-to-rocq. Take a copy, put it at the same path in your own repository, and replace the rules that are about this project with yours.
curl -O https://raw.githubusercontent.com/plclub/hs-to-rocq/master/CLAUDE.mdgit clone --depth 1 https://github.com/plclub/hs-to-rocqWrote this? Show the measurements
A badge with what this costs and how it scanned, read live from this page, so it follows the numbers instead of freezing them. Markdown for a README, HTML for a documentation site or a project page.
[](https://agentmods.dev/instructions/plclub/hs-to-rocq/claude-md)<a href="https://agentmods.dev/instructions/plclub/hs-to-rocq/claude-md"><img src="https://agentmods.dev/badge/instructions/plclub/hs-to-rocq/claude-md/github.svg" alt="Measured on agentmods" height="20"></a>Or the 80×15 button, for a site that already has a row of RSS and ATOM ones. Only the verdict fits; the numbers stay here.
<a href="https://agentmods.dev/instructions/plclub/hs-to-rocq/claude-md"><img src="https://agentmods.dev/badge/instructions/plclub/hs-to-rocq/claude-md.svg" alt="Reviewed on agentmods" width="80" height="20"></a>What it costs to keep this loaded
Counted locally with the o200k_base tokenizer, which is exact for GPT models; Claude uses its own tokenizer and its counts differ. Treat this as one consistent yardstick across the catalogue rather than a bill. Prices are per million input tokens.
| Model | Per session | Once invoked |
|---|---|---|
| Fable 5.1 | $0.09560 | $0.09560 |
| Opus 5.5 | $0.03824 | $0.03824 |
| Sonnet 5.5 | $0.01912 | $0.01912 |
| Haiku 4.5 | $0.00956 | $0.00956 |
Grade B, and why
hs-to-rocq CLAUDE.md scanned grade B with 1 finding against 26 rules in 11 categories — prompt injection, anti-refusal, data exfiltration, privilege escalation, supply chain, agent snooping, system-prompt leakage, SSRF and excessive agency — measured today.
A static scan of the body, not an audit. Every finding is printed with the line that produced it so you can judge whether it matters here. A mod is markdown that instructs an agent; that is exactly why what it instructs is worth reading.
Asks for rootmediumPrivilege escalation
A mod that escalates privileges can change anything on the machine, not only the project.
**Container job gotcha**: Container jobs use `--allow-different-user` for stack commands (ownership mismatch between host-mounted workspace and container user). For docker-coq-action, use `before_script` with `sudo chown How it starts
The opening of the file, as written. The whole thing — 275 lines — stays where its author put it; the contents beside it link to each section on GitHub.
CLAUDE.md
This file provides guidance to Claude Code (claude.ai/code) when working with code in this repository.
Project Overview
hs-to-rocq converts Haskell source code to Coq (Gallina) using the GHC API. It is part of the DeepSpec/CoreSpec project. The tool parses Haskell via GHC, applies user-specified "edits" to guide the translation, and pretty-prints valid Coq output.
- Current targets: GHC 9.10.3; Coq 8.20 (default) or Rocq 9.0 via
--target-version(branchghc910-coq820) - Languages: Haskell (the tool, ~14K LOC in
src/), Coq (generated output and proofs)
Build Commands
stack build # Build hs-to-rocq executable
stack exec hs-to-rocq -- -e edits -o output/ Input.hs # Run on a file
make # Build base + base-thy + containers
make -C examples/base-src vfiles # Re-generate base/ from Haskell sources
make -C examples/tests # Unit tests (.hs → .v → coqc)
make -C examples/base-tests # Tests requiring base/
make -C examples/rocq9.0 # Rocq 9.0 base + shared unit tests
make -C examples/containers # containers lib + theories (regenerates + builds)
make -C examples/transformers # transformers lib
make -C examples/ghc clean && make -C examples/ghc # Regenerate+compile GHC lib + theories
cd examples && ./boot.sh # Full bootstrap (all examples)
# Individual Coq dirs: cd <dir> && coq_makefile -f _CoqProject -o Makefile && make -j
Use relative path instead of absolute path when cd to a directory.
CI commands
/ci— run CI checks locally, report pass/fail/ci-fix— run CI checks, diagnose and fix failures, commit fixes
Both commands use .claude/commands/ci.md as their shared catalog of all seven
workflow jobs, including direct, harness, concurrent, and both Rocq checks. The
compiler jobs use separate Coq 8.20 and Rocq 9.0 environments. Expected test
failures already return zero; every nonzero Make status needs investigation.
When changing either command or the workflow, run
stack exec -- runghc -package=yaml examples/tests/checks/CiCatalog.hs --self-test.
This build-haskell guard checks catalog coverage, delegation, failure masking,
shell syntax, and regressions without running the documented builds.
What this file has done since we first saw it
Hashed on every crawl. A supply-chain change to an agent config is a question of when, not whether, so the history is kept rather than the latest state alone.
- today Changed · +60 lines · +3,551 tokens per session 0a13c2948bad
- 1mo ago First seen · 215 lines · 6,009 tokens per session scan B 139c9c3ee4fe
hs-to-rocq CLAUDE.md is an instructions file published in the GitHub repository plclub/hs-to-rocq (96 stars, last pushed yesterday), licensed MIT. It adds 9,560 tokens to every session, about $0.0382 per session on Opus 5.5. A static security scan graded it B with 1 finding (asks for root). No closer match exists in the catalogue, so it is treated as the original; first seen 2026-09-01.
Other instructions, from other repositories
vscode buildNext.instructions.md
Working notes and architecture documentation for the new esbuild-based build system in build/next. Use when making changes to the new build pipeline (transpile/bundle commands, NLS plugin, source-map handling, resource copying, or self-hosting watch tasks).
next.js AGENTS.md
AGENTS.md instructions for vercel/next.js, covering next.js development guide, codebase structure, monorepo overview, core package: packages/next and other important packages.
vscode oss-third-party-notices.instructions.md
Instructions for microsoft/vscode, covering vs code oss third-party-notices pipeline, architecture, pipeline flow in ci, cache eligibility and rollout and applying the notice (cutover).
langchain AGENTS.md
AGENTS.md instructions for langchain-ai/langchain, covering global development guidelines for the langchain monorepo, corridor security analysis, project architecture and context, monorepo structure and development tools & commands.
vscode copilot-instructions.md
Copilot instructions for microsoft/vscode, covering vs code copilot instructions, project overview, root folders, core architecture (src/ folder) and built-in extensions (extensions/ folder).
deepseek-harness AGENTS.md
AGENTS.md instructions for deepseek-ai/deepseek-harness, covering agents.md, pre-stable apis and released session data, repository layout, commands and host sandbox failures.