package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

The debugger receives requests by calling read_cmd to get Actions. Each Action may return one or more responses as Answers by calling submit_answer. Many of them return a single Answer or no Answer, but a single step may generate any number of Outputs.

Debugger initialization has the following steps: -> Coq sends Answer.Init <- IDE sends zero or more initialization requests such as Action.UpdBpts <- IDE sends Action.Configd

Stopping in the debugger generates Answer.Prompt and Answer.Goal messages, at which point the IDE will typically call GetStack and GetVars. When the IDE sends with StepIn..Continue, the debugger will execute more code. At that point, Coq won't try to read more messages from the IDE until the debugger stops again or exits.

type t =
  1. | StepIn
  2. | StepOver
  3. | StepOut
  4. | Continue
  5. | Skip
  6. | Interrupt
  7. | Help
  8. | UpdBpts of ((string * int) * bool) list
  9. | Configd
  10. | GetStack
  11. | GetVars of int
  12. | RunCnt of int
  13. | RunBreakpoint of string
  14. | Command of string
  15. | Failed
  16. | Ignore
val parse : string -> (t, string) result