• Guillaume Melquiond's avatar
    Keep track of "ITP" provers and avoid running such provers on unedited proofs. · 406f058e
    Guillaume Melquiond authored
    When the user wants to write a Coq proof, she needs to run Coq on the goal,
    wait five seconds for it to fail (it will fail, otherwise there is no point
    in running Coq on this goal: another prover would have succeeded already),
    and finally edit it. This is a waste of time. So goals run with an
    interactive prover are now marked as unknown until their file is edited.
    Interactive provers could have been detected by a nonempty "editor" string,
    but there are interactive provers that don't have dedicated editors, and
    there might be automated provers with dedicated user interfaces. So a new
    field was added to prover descriptions.
    TODO: actually run the editor when there is only one selected goal,
    rather than keeping the current three-click method of editing proofs.
autodetection.ml 6.65 KB