Troubleshooting

Troubleshooting usually moves from explicit, localized tool feedback toward more implicit, reasoning-derived, and potentially non-local findings:

• Categorize the Issue: classify whether the problem is still local and tool-facing, or has become a deeper proof-time or semantic issue.
• Diagnose, Explain, and Evaluate: start with the smallest local explanation and the smallest local experiment, then escalate to deeper candidate causes only after the simpler, more local ones have been explored, explained, or eliminated.
• Propagate Fixes Incrementally: validate locally before hoisting, generalizing, or widening scope; broader changes can induce churn, larger rebuilds, and unrelated breakage.

Categorize the Issue

Rocq catches many issues during sentence processing, including typechecking. Some of those checks rely on subtle mechanisms (e.g. typeclass-driven search, conversion and unification, and extensible notations and notation scopes), which can still produce syntactically valid but unexpectedly shaped terms.

Local, Immediate Issues

• Tool issues: problems while preparing generated Rocq artifacts for C++ code, completing builds, using the editor environment, or working with the scaffold tool. If you need to re-orient on the normal project flow, revisit the Quick Start.
• Syntax or typechecking issues: failures while Rocq processes the next sentence, whether inside a proof or while defining terms, instances, sections, modules, or contexts. These often involve imports and namespaces, even when the immediate failure surfaces as a typechecking or lookup error.
• Tactic failures: Rocq feedback that a tactic sentence is not accepted, often because the tactic is malformed, the applied fact does not match the goal, or some local tactic invariant is violated.

Deeper, Reasoning-Derived Issues

• Proof issues: some proof issues only become clear once you inspect the resulting state and the reasoning path that produced it.
  • Strategy gotchas: proof families with a clear happy path, where locally legal but poorly-aligned steps can make the rest of the argument much more manual, brittle, or opaque than it needs to be.
  • Surprising or incorrect proof-state transitions: confusing, unexpectedly stuck, or incorrectly transformed proof states, including over-aggressive automation steps or bad existential instantiations that leave the remaining goals unprovable.
• Modelling / Specification / Code Issues / Bugs: mismatches in formalization style, information hiding, abstraction boundaries, or client-versus-implementer needs, as well as outright mistakes in reps, specs, or the underlying C++ code.

Diagnose, Explain, and Evaluate

Prefer the smallest local explanation and the smallest local experiment first. Start with the immediate messages from Rocq, scaffold, dune, or related tools; if those do not fully explain the behavior, move toward reasoning-based debugging of proof states, automation behavior, and upstream semantic choices.

• Local tool feedback first: separate parser, build, editor-environment, syntax, typechecking, and tactic failures from deeper proof-state causes before widening the debugging scope.
• Proof issues: once local sentence-processing failures are ruled out, decide whether the real problem is the proof path itself or the behavior of the resulting state.
  • Strategy gotchas: check whether the current proof family has a better-structured happy path before committing to a state that is technically valid but much rougher to finish.
  • Surprising or incorrect proof-state transitions: inspect how the proof state evolved, compare it against what you expected, and evaluate the smallest candidate local fixes.
• Modelling / Specification / Code Issues / Bugs: check whether the real cause lies in formalization choices, information hiding, spec or rep phrasing, client-versus-implementer boundaries, or an actual bug in the model or the underlying C++ code.

Contents

• Proof Strategy Gotchas
• Diagnosing Surprising or Incorrect Proof-State Transitions
  • Dealing with Missing Type Instances