1. 08 Feb, 2012 2 commits
  2. 31 Jan, 2012 1 commit
  3. 30 Jan, 2012 1 commit
  4. 25 Jan, 2012 2 commits
    • François Bobot's avatar
      Session doesn't use anymore prover id. · 2e2e0d83
      François Bobot authored
      Prover ids are only used for the command line option "-P".
      The user can choose what he wants (they must be unique)
      The prover name and version should not be modified. If someone want to
      test different command line options for a prover he can use the
      "alternative" field.
      
      If someone want to replay an external proof but he doesn't have the
      corresponding prover (same name,version,alternative), why3ide ask for
      a replacement among the known provers. The choice can be saved.
      2e2e0d83
    • François Bobot's avatar
      ac98a7a4
  5. 19 Jan, 2012 1 commit
    • François Bobot's avatar
      Session rewrite fix : · 13c872fa
      François Bobot authored
       - goal name are correctly printed when no explanation are provided
       - explanation becomes an abstract type
      13c872fa
  6. 18 Jan, 2012 2 commits
  7. 03 Jan, 2012 1 commit
    • François Bobot's avatar
      new session · 49c19a38
      François Bobot authored
      Split session in two :
      Session : an API for managing session without running provers
      Session_scheduler : an API for running provers asynchronously
      
      All the global states have been removed.
      
      A session must be first read, which give a session without task.
      Afterward it must be updated to the current state of the files with
      some environnement and configuration.
      
      printer and iterator are provided for session.
      
      Session_tools : some useful functions on session.
      
      Smoke detector : not anymore integrated to session. Just add the
            transformation "smoke_detector_top" or "smoke_detector_deep" to
            all the valid proof attempt.
      
      prover_id are not yet removed but all is in place in session for that.
      49c19a38
  8. 01 Dec, 2011 1 commit
  9. 27 Nov, 2011 1 commit
  10. 14 Nov, 2011 1 commit
    • MARCHE Claude's avatar
      heuristic for time limit of proof replay · 14a1e9e2
      MARCHE Claude authored
      the time limit for the replay is the max of the time limit
      given initially and twice the time taken by the prover
      (if the result was "valid")
      
      E.g, if Alt-Ergo said valid in 4.9 seconds, for an initial limit of 5,
      then the replay will give 10 seconds
      14a1e9e2
  11. 21 Oct, 2011 1 commit
  12. 30 Sep, 2011 1 commit
  13. 28 Sep, 2011 1 commit
  14. 24 Sep, 2011 2 commits
    • 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.
      406f058e
    • MARCHE Claude's avatar
      Improved monitoring of running proofs · 841b97b2
      MARCHE Claude authored
      841b97b2
  15. 23 Sep, 2011 1 commit
  16. 22 Sep, 2011 1 commit
  17. 20 Sep, 2011 3 commits
  18. 18 Sep, 2011 1 commit
  19. 15 Sep, 2011 5 commits
  20. 14 Sep, 2011 1 commit
  21. 11 Sep, 2011 2 commits
  22. 07 Sep, 2011 1 commit
  23. 20 Aug, 2011 1 commit
    • Guillaume Melquiond's avatar
      Modify the source buffer so that the filename is used for selecting syntax... · d9caac0a
      Guillaume Melquiond authored
      Modify the source buffer so that the filename is used for selecting syntax highlighting rather than always using why.
      
      This ensures that C files (coming from Jessie) are not uniformly blue due to pointer deferencing "(*ptr)".
      For unrecognized files (e.g. Jesse files), the IDE falls back to the old approach, that is, using Why highlighting.
      d9caac0a
  24. 11 Aug, 2011 2 commits
  25. 04 Jul, 2011 1 commit
  26. 03 Jul, 2011 1 commit
  27. 02 Jul, 2011 2 commits