• Sylvain Dailler's avatar
    Added replay. To be checked/tested. · c80328b7
    Sylvain Dailler authored
    * call_provers.ml
    (prover_update): Adding unimplemented errors that reflects the cases of
    proof_attempt_status. Otherwise, proof_attempt_status is a list of cases
    that are never reached.
    * controller_itp.ml
    (proof_attempt_status): Added Uninstalled case in proof_attempt_status.
    Launched in replay when asked to replay something not installed.
    (print_trans_status): Adding a ! when proof is valid for debugging
    reasons.
    (report): Added a report type for replay reporting of differences.
    (print_report): printing function for report.
    (replay_print): callback used with replay to print the report at the end.
    (replay): Function that replays all proof attempts of the session.
    
    * session_itp.ml
    (session_iter_proof_attempt): Added the proofNodeID the fold function
    for convenience.
    * why3shell.ml
    (test_replay): Added to test replay.
    c80328b7
why3shell.ml 25 KB