1. 15 Feb, 2019 2 commits
    • Sylvain Dailler's avatar
      Factor abnormal transformation exceptions under is_fatal · 1d8789b7
      Sylvain Dailler authored
      When reloading, fatal transformations should be notified to the user but
      should not make the whole reload fail
      1d8789b7
    • Sylvain Dailler's avatar
      fix #274 · ead51b74
      Sylvain Dailler authored
      When applying a transformation without arguments, this checks that
      arguments are indeed not provided. If they are, it now raises the same
      exception as transformation with too many arguments.
      
      Also update CHANGES with recent changes.
      ead51b74
  2. 13 Feb, 2019 1 commit
  3. 11 Feb, 2019 1 commit
  4. 08 Feb, 2019 1 commit
  5. 06 Dec, 2018 1 commit
  6. 04 Dec, 2018 1 commit
  7. 30 Nov, 2018 1 commit
  8. 13 Nov, 2018 2 commits
  9. 23 Oct, 2018 1 commit
  10. 18 Oct, 2018 1 commit
  11. 08 Oct, 2018 1 commit
  12. 04 Oct, 2018 1 commit
    • Guillaume Melquiond's avatar
      Change time limit computation. · cbfb1d83
      Guillaume Melquiond authored
      For a measured time of 0.49 second, a prover would only get 1 second to
      replay the proof, i.e., half of the expected 1.98 seconds. The time limit
      is now rounded to nearest to prevent this underestimation on fast proofs.
      cbfb1d83
  13. 02 Oct, 2018 1 commit
    • Sylvain Dailler's avatar
      Fix issue #190 · c1dde87a
      Sylvain Dailler authored
      Exceptions from transformations are of two kinds:
      - fatal exception which are then raised into a popup in the ide
      - normal exception which appears in the message view
      c1dde87a
  14. 01 Oct, 2018 2 commits
  15. 10 Sep, 2018 4 commits
  16. 30 Jul, 2018 1 commit
  17. 17 Jul, 2018 1 commit
    • Sylvain Dailler's avatar
      R531-011 minor refactoring · 8f5782a9
      Sylvain Dailler authored
      Introduce a record type instead of large tuple for queue of scheduled
      proof attempts
      
      Change-Id: If4d4284a78d5d828bb06705f2628ea341d7a1d64
      (cherry picked from commit 1070b12841adc076ba67193722b250c81a1a697c)
      8f5782a9
  18. 14 Jun, 2018 1 commit
  19. 28 May, 2018 1 commit
  20. 07 May, 2018 1 commit
  21. 04 May, 2018 1 commit
  22. 09 Apr, 2018 1 commit
  23. 04 Apr, 2018 1 commit
  24. 28 Mar, 2018 2 commits
  25. 27 Mar, 2018 1 commit
    • Sylvain Dailler's avatar
      Add debug keep_vcs: allow to use a given filename to save prover files. · 979cf05c
      Sylvain Dailler authored
      It is now possible to give an optional argument to schedule_proof_attempt
      so that (when in debug mode) the file given is used to store the generated
      input file of the prover. In non debug mode, the file given to
      schedule_proof_attempt is used but removed after the call to the prover.
      
      Currently, no file is ever given to schedule_proof_attempt but this can be
      used by people using Why3 as a backend.
      979cf05c
  26. 26 Mar, 2018 1 commit
  27. 07 Mar, 2018 1 commit
    • MARCHE Claude's avatar
      solve a few issue about proof edition · 82e3e856
      MARCHE Claude authored
      - use the default editor if no specific editor known
      - keep the former result after edition, although obsolete
      
      Note that the "default_editor" setting is moved from the IDE config to
      the main config section
      82e3e856
  28. 16 Feb, 2018 1 commit
  29. 15 Feb, 2018 2 commits
  30. 14 Feb, 2018 1 commit
  31. 22 Jan, 2018 1 commit
  32. 19 Jan, 2018 1 commit
    • MARCHE Claude's avatar
      Improved copy-paste functionality · a97edee6
      MARCHE Claude authored
      - copy from a transformation to a proof node works, adding
        the transformation below the target node
      
      - when copied transformation as less or more subgoals, then
        only the first subgoals are copied
      
      - explicit error message in case of invalid copy
      a97edee6