1. 09 Apr, 2012 1 commit
  2. 23 Mar, 2012 1 commit
  3. 09 Mar, 2012 1 commit
  4. 08 Mar, 2012 1 commit
  5. 29 Feb, 2012 2 commits
  6. 22 Feb, 2012 1 commit
    • Andrei Paskevich's avatar
      make api of maps/sets more consistent · 33bb423f
      Andrei Paskevich authored
      - change takes function as the first argument
      - add_new takes exception as the first argument
      - find_default is renamed to find_def and takes the default value
        as the first argument
      - find_option is renamed to find_opt (to align with find_exn and find_def)
      - default_option is renamed def_option
      33bb423f
  7. 21 Feb, 2012 1 commit
  8. 13 Feb, 2012 1 commit
  9. 01 Feb, 2012 2 commits
    • François Bobot's avatar
      why3session info : add --edited-files option which · 890ca844
      François Bobot authored
      print all the edited files which appear in the session.
      
      In conjonction with --print0 which prints '\000' instead of '\n' that
      give a safe way to "git add" all the edited files of a session:
      
      why3session info --edited-files --print0 vstte12_bfs.mlw |xargs -0 git add
      
      Since why3session accept the why3session.xml (it uses the basename as
       session directory) you can add all the edited file of all the session
      saved in a git repository with:
      
      git ls-files -z |grep -z -e "why3session.xml$" |xargs -0 why3session info --edited-files --print0 | xargs -0 git add
      890ca844
    • François Bobot's avatar
      ab24b3e2
  10. 25 Jan, 2012 1 commit
    • 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
  11. 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
  12. 27 Dec, 2011 1 commit
  13. 17 Nov, 2011 1 commit
  14. 11 Nov, 2011 1 commit
  15. 31 Oct, 2011 2 commits
  16. 13 Oct, 2011 1 commit
  17. 16 Sep, 2011 1 commit
  18. 28 Jul, 2011 1 commit
  19. 02 Jul, 2011 1 commit
  20. 01 Jul, 2011 2 commits
  21. 30 Jun, 2011 1 commit
  22. 31 May, 2011 1 commit
  23. 24 May, 2011 1 commit
  24. 20 May, 2011 1 commit
  25. 18 May, 2011 1 commit
  26. 17 May, 2011 1 commit
  27. 15 May, 2011 1 commit
  28. 09 May, 2011 1 commit
  29. 05 May, 2011 1 commit
  30. 29 Apr, 2011 1 commit
  31. 22 Apr, 2011 1 commit
    • François Bobot's avatar
      autodetection : simplify the semantics of the file provers-detection-data.conf · ef43f13a
      François Bobot authored
      * all the provers with the same prover_id are threated as one prover,
      * the first description of a prover in the file pdd.conf which have an
        executable with a good version is used,
      * the order used to test the executable (exec) inside a prover description
        is not specified,
      * a version_bad allows to forbid a version.
      * a version_ok matches no warning is printed
      * a version_old matches a warning is printed
      * if no version matches a warning is printed
      ef43f13a
  32. 21 Apr, 2011 1 commit
  33. 11 Apr, 2011 1 commit
    • Guillaume Melquiond's avatar
      Fix display of error messages. · a8fe9a2b
      Guillaume Melquiond authored
      Before:
      File "b/../b.why", line 7, characters 36-37This term has type int but is expected to have type real
      
      After:
      File "b/../b.why", line 7, characters 36-37:
      This term has type int but is expected to have type real
      a8fe9a2b
  34. 05 Mar, 2011 1 commit
  35. 04 Mar, 2011 1 commit
  36. 24 Feb, 2011 1 commit