Make sertop respond consistently to SIGINT

[elidupree]

Currently, these notes appear to be the most detailed documentation on interrupting sertop:

Interrupting

1. The IDE must send an interrupt signal to sertop.
2. The IDE must process all the pending feedback until getting the Break message.
3. The IDE must then cancel non-desired states.

And this code appears to be the full code for handling interrupts:

  (* Follow the same approach than coqtop for now: allow Coq to be
   * interrupted by Ctrl-C. Not entirely safe or race free... but we
   * trust the IDEs to send the signal on coherent IO state.
   *)
  Sys.catch_break true;

[...]

  (* Main loop *)
  let rec loop ctx =
    let quit, ctx =
      try
        [...]
      with Sys.Break -> false, ctx
    in
    if quit then () else (loop [@ocaml.tailcall]) (incr_cmdid ctx)
  in loop ctx

However, in practice, these do not match: sertop does not always send the Break message after receiving an interrupt. "Not entirely safe or race free" appears to be a practical problem as well as a theoretical one. As far as I can tell from experimentation:

• If there is no command running, sertop sends Sys.Break (not a sexp, just Sys.Break on its own line).
• If there is a command running:
  • usually, sertop sends a sexp of a CoqExn saying User interrupt., followed by a Completed. (Or sometimes the CoqExn is an Anomaly instead because Coq is also buggy.)
  • sometimes sertop sends Sys.Break as above (perhaps because the interrupt didn't arrive before the command finished).
  • sometimes sertop does not send any acknowledgement of the interrupt at all (and may or may not send a Completed).

And this is WITH being careful to only send the interrupt after receiving an Ack (if I send the interrupt before the Ack, I sometimes also get a mess of sexp parse errors, perhaps indicating that sertop was interrupted in the middle of parsing my command).

Overall, I think the current implementation only works reliably enough that it will usually not fail catastrophically in the use case of "a human occasionally thinks a command is taking too long and sends an interrupt manually" (because at that point, it's very unlikely that the command will happen to finish at the moment the interrupt arrives, so the interrupt will consistently hit Coq code and be caught as a Coq exception). But I'm trying to use it programmatically (for example, interrupting any tactic that runs for longer than 10ms). In this context, I'm often getting the "no acknowledgment of the interrupt" case after only dozens of interrupts.

I'm not familiar with interrupt handling in OCaml, but it seems like the logical approach would be to set an interrupt handler that does not trigger exceptions in arbitrary SerAPI functions, but only in specific places (such as during Coq commands), and otherwise simply sets a flag to remember to interrupt at the next time it reaches a location in the code that explicitly written to be safely interruptible.

[elidupree]

As another note, all the commands I've been testing with are ones that finish normally if you don't interrupt them (generally not running longer than 80ms naturally), so none of the issues above are a case of "there was an infinite loop that was unable to be interrupted". It seems to me that sertop does promptly either complete or abort the command, it just doesn't always acknowledge that it has done so.

[ejgallego]

Sorry @elidupree for the long time to reply to this issue. The new version of SerAPI relies on interruptions constantly and it has reworked support, will look into this.