1. 25 Jun, 2017 2 commits
  2. 23 Jun, 2017 1 commit
  3. 24 May, 2017 1 commit
  4. 23 May, 2017 1 commit
    • Sylvain Dailler's avatar
      Adding Edit_req · c0d087be
      Sylvain Dailler authored
      Unfinished work to retrieve manual proofs.
      (minor) added a use case for stack_trace
      c0d087be
  5. 12 May, 2017 1 commit
  6. 10 May, 2017 4 commits
  7. 05 May, 2017 2 commits
  8. 03 May, 2017 1 commit
  9. 28 Apr, 2017 2 commits
  10. 26 Apr, 2017 1 commit
  11. 22 Apr, 2017 2 commits
  12. 21 Apr, 2017 1 commit
  13. 18 Apr, 2017 1 commit
  14. 14 Apr, 2017 1 commit
  15. 11 Apr, 2017 1 commit
  16. 06 Apr, 2017 1 commit
  17. 09 Jan, 2017 1 commit
  18. 16 Dec, 2016 1 commit
  19. 09 Dec, 2016 1 commit
  20. 07 Dec, 2016 1 commit
    • Sylvain Dailler's avatar
      Clear command after request is sent. · 51c0880b
      Sylvain Dailler authored
      (ide) new_node returns the row_ref of new node. So that we can go to
      the ggoal generated by transformation (convenience).
      Changed the update of the proof_status in controller_itp. update_node
      functions now take a callback called notification which is actually
      P.notify (node_change).
      Put type any inside session_itp.ml.
      51c0880b
  21. 01 Dec, 2016 2 commits
  22. 24 Nov, 2016 1 commit
    • Sylvain Dailler's avatar
      Adding a known_id function for prineter in Ident. · f5a07e19
      Sylvain Dailler authored
      Adding a forgeting function for printing variables on exceptions.
      Should do the same at least for patterns.
      Adding printing functions from why3printer.
      Changing exception in transformation so that they
      return terms not strings.
      f5a07e19
  23. 22 Nov, 2016 1 commit
  24. 18 Nov, 2016 1 commit
  25. 17 Nov, 2016 1 commit
  26. 16 Nov, 2016 1 commit
  27. 15 Nov, 2016 1 commit
  28. 10 Nov, 2016 1 commit
  29. 09 Nov, 2016 1 commit
  30. 04 Nov, 2016 2 commits
    • Sylvain Dailler's avatar
    • 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
  31. 28 Oct, 2016 1 commit