rocq-build-troubleshoot
Installation
SKILL.md
Rocq Build Troubleshoot
Use this skill when a .v file fails to compile and the goal is a minimal targeted fix.
Scope
- Repository:
RocqOfRust - Commands use project flags:
-R . RocqOfRust -impredicative-set - Prefer single-file checks first, then dependency checks.
Workflow
- Reproduce exactly:
coqc -R . RocqOfRust -impredicative-set path/to/file.v
- If error references missing module/loadpath:
- Add explicit
Require Import ...in the failing file. - Do not rely on removed aggregator modules.
- Prefer per-function imports in
revm/revm_interpreter/instructions/{links,simulate}/....