1. 05 Apr, 2017 2 commits
  2. 18 Jan, 2017 1 commit
    • Sylvain Dailler's avatar
      Json file to Json_base for compatibility with js_of_ocaml. · a478fd6d
      Sylvain Dailler authored
      Entry in Makefile to compile ocaml code to js (like trywhy3).
      Put why3webserver parsing/printing into Json_util.
      Split Itp_server into Itp_communication and Itp_server to isolate
      notification and request from the rest in an attempt to reduce
      dependencies.
      a478fd6d
  3. 12 Jan, 2017 1 commit
  4. 05 Jan, 2017 1 commit
  5. 15 Dec, 2016 1 commit
  6. 08 Dec, 2016 2 commits
  7. 05 Dec, 2016 1 commit
  8. 29 Nov, 2016 1 commit
    • Sylvain Dailler's avatar
      Third commit. For saving. · ee0cf016
      Sylvain Dailler authored
      Change many function from gconfig.ml to remove ref to Whyconf.
      Add protocol file.
      Add whats needed in an adhoc way.
      Need cleaning. Compile but fails.
      ee0cf016
  9. 23 Nov, 2016 1 commit
    • Sylvain Dailler's avatar
      Add a name_table in proof_node. · e0d6b38d
      Sylvain Dailler authored
      Add a name_table in printer_args.
      Put the definition of name_table in task.ml.
      Build_name_tables only called once in proof_node creation.
      Modified the rest accordingly.
      e0d6b38d
  10. 17 Nov, 2016 3 commits
  11. 15 Nov, 2016 1 commit
  12. 10 Nov, 2016 1 commit
  13. 09 Nov, 2016 3 commits
  14. 08 Nov, 2016 1 commit
    • Sylvain Dailler's avatar
      Adding a search command. · 0b8634b0
      Sylvain Dailler authored
      Added a last set which is build at the same time of the name_tables which
      is a map from id to list of decls where id is used. This has to be tested
      if this is actually efficient (time and memory). If not, we can still
      disallow it with a boolean.
      0b8634b0
  15. 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
  16. 02 Nov, 2016 1 commit
  17. 28 Oct, 2016 1 commit
  18. 27 Oct, 2016 1 commit
  19. 26 Oct, 2016 2 commits
  20. 24 Oct, 2016 1 commit
  21. 21 Oct, 2016 2 commits
  22. 20 Oct, 2016 1 commit
  23. 12 Oct, 2016 1 commit
  24. 11 Oct, 2016 1 commit
  25. 07 Oct, 2016 4 commits
  26. 06 Oct, 2016 1 commit
  27. 04 Oct, 2016 2 commits