rocq-build-troubleshoot
This workflow helps diagnose and resolve compilation errors in RocqOfRust files by adjusting imports and argument signatures.
Install
mkdir -p .claude/skills/rocq-build-troubleshoot && curl -L -o skill.zip "https://agentskills.codes/api/skills/download/3400" && unzip -o skill.zip -d .claude/skills/rocq-build-troubleshoot && rm skill.zipInstalls to .claude/skills/rocq-build-troubleshoot
Activation
This is the description your AI agent reads to decide when to run this skill — the better it matches your request, the more reliably it fires.
Fast workflow to diagnose and fix Rocq/Coq compile errors in this repository, especially missing imports after links/simulate splits and per-file compile checks.Key capabilities
- →Reproduce Rocq/Coq compile errors for a .v file
- →Add explicit `Require Import` statements for missing modules
- →Align argument signatures for `run_*` calls
- →Use record notation with typed zeros for `Range` literals
- →Recompile touched .v files
How it works
This skill provides a workflow to diagnose and fix Rocq/Coq compile errors in `.v` files by guiding the user through reproducing errors, adding imports, aligning arguments, and recompiling.
Inputs & outputs
When to use rocq-build-troubleshoot
- →Fix Rocq compilation errors
- →Resolve missing module imports
- →Debug argument mismatch in Rocq functions
About this skill
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}/....
- If error is argument-order/type mismatch in
run_*call:
- Compare the local
run_*instance signature in.../links/.... - Align call order exactly; remove placeholder
_arguments unless required by implicit params.
- If
Rangeliterals fail type inference:
- Use record notation with typed zeros:
{|
Range.start := (0 : usize);
Range.end_ := (0 : usize)
|}
- Recompile touched file(s):
coqc -R . RocqOfRust -impredicative-set path/to/file.v
- Optional dependency sanity check:
make path/to/file.vo
Guardrails
- Keep fixes minimal and local.
- Do not reintroduce removed aggregators.
- Preserve
Admittedwhere the project intentionally keeps placeholders. - If proving
_eqfails, check semantic alignment before attemptingQed.
Limitations
- →The scope is limited to the `RocqOfRust` repository.
- →Fixes should be minimal and local.
- →Do not reintroduce removed aggregators.
How it compares
This skill offers a targeted workflow for fixing specific Rocq/Coq compile errors within the `RocqOfRust` repository, focusing on minimal, local changes, unlike general Coq debugging.
Compared to similar skills
rocq-build-troubleshoot side by side with the closest alternatives in the catalog.
| Skill | Installs | Updated | Safety | Difficulty |
|---|---|---|---|---|
| rocq-build-troubleshoot (this skill) | 1 | 6mo | Review | Intermediate |
| memory-safety-patterns | 4 | 4mo | No flags | Advanced |
| debug-cli | 1 | 8mo | Review | Intermediate |
| fix-clippy | 3 | 6mo | No flags | Beginner |
Try saying
Example prompts that trigger this skill in your AI assistant.
More by formal-land
View all by formal-land →You might also like
memory-safety-patterns
sickn33
Implement memory-safe programming with RAII, ownership, smart pointers, and resource management across Rust, C++, and C. Use when writing safe systems code, managing resources, or preventing memory bugs.
debug-cli
antinomyhq
Use when users need to debug, modify, or extend the code-forge application's CLI commands, argument parsing, or CLI behavior. This includes adding new commands, fixing CLI bugs, updating command options, or troubleshooting CLI-related issues.
fix-clippy
quickwit-oss
Fix all clippy lint warnings in the project
debug-lldb
regenrek
Capture and analyze thread backtraces with LLDB/GDB to debug hangs, deadlocks, UI freezes, IPC stalls, or high-CPU loops across any language or project. Use when an app becomes unresponsive, switching contexts stalls, or you need thread stacks to locate lock inversion or blocking calls.
handling-rust-errors
hashintel
HASH error handling patterns using error-stack crate. Use when working with Result types, Report types, defining custom errors, propagating errors with change_context, adding context with attach, implementing Error trait, or documenting error conditions in Rust code.
rust-router
actionbook
CRITICAL: Use for ALL Rust questions including errors, design, and coding. HIGHEST PRIORITY for: 比较, 对比, compare, vs, versus, 区别, difference, 最佳实践, best practice, tokio vs, async-std vs, 比较 tokio, 比较 async, Triggers on: Rust, cargo, rustc, crate, Cargo.toml, 意图分析, 问题分析, 语义分析, analyze intent, question analysis, compile error, borrow error, lifetime error, ownership error, type error, trait error, value moved, cannot borrow, does not live long enough, mismatched types, not satisfied, E0382, E0597, E0277, E0308, E0499, E0502, E0596, async, await, Send, Sync, tokio, concurrency, error handling, 编译错误, compile error, 所有权, ownership, 借用, borrow, 生命周期, lifetime, 类型错误, type error, 异步, async, 并发, concurrency, 错误处理, error handling, 问题, problem, question, 怎么用, how to use, 如何, how to, 为什么, why, 什么是, what is, 帮我写, help me write, 实现, implement, 解释, explain