1. 18 Nov, 2011 1 commit
  2. 17 Nov, 2011 1 commit
  3. 11 Nov, 2011 1 commit
  4. 09 Nov, 2011 1 commit
  5. 04 Nov, 2011 1 commit
  6. 27 Oct, 2011 1 commit
  7. 26 Oct, 2011 1 commit
  8. 13 Oct, 2011 1 commit
  9. 30 Sep, 2011 1 commit
    • Andrei Paskevich's avatar
      add the option --realize to Main · 9ab0704b
      Andrei Paskevich authored
      How to use it:
      
          why3 --realize -D drivers/coq-realize.drv -T real.Real -o .
      
              produces Real.v in the current directory
      
          why3 --realize -D drivers/coq-realize.drv -T real.Real
      
              produces real/Real.v in the loadpath near real.why
              (the directory "real" must exist)
      
      If a realization file is already there, it is passed to
      the printer in order to preserve the proofs.
      
      Instead of -D <driver_file>, you can use -P <prover>,
      if that prover uses a corresponding driver. However,
      the prover itself is not used.
      
      You can only realize theories from the loadpath.
      
      At the moment, coq-realize.drv is the only driver
      capable to realize theories in some sensible way.
      For any other driver, the results may be funny.
      
      Realization of WhyML modules is not possible so far.
      
      Realization may break if you directories and filenames
      contain non-alphanumeric symbols.
      
      The whole thing is in very preliminary stage.
      Use with caution.
      9ab0704b
  10. 29 Sep, 2011 4 commits
  11. 24 Sep, 2011 1 commit
    • 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
  12. 18 Sep, 2011 1 commit
  13. 17 Sep, 2011 1 commit
  14. 05 Jul, 2011 1 commit
  15. 02 Jul, 2011 4 commits
  16. 01 Jul, 2011 1 commit
  17. 29 Jun, 2011 1 commit
  18. 11 Jun, 2011 1 commit
    • Andrei Paskevich's avatar
      a little refactoring in Env · b8dcebfc
      Andrei Paskevich authored
      - create_env_of_loadpath is now provided in Env instead of Lexer
      - find_channel functions now depend on format to determine the
        suitable extensions
      b8dcebfc
  19. 24 May, 2011 1 commit
  20. 22 May, 2011 2 commits
  21. 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
  22. 21 Apr, 2011 3 commits
  23. 31 Mar, 2011 1 commit
  24. 15 Mar, 2011 1 commit
  25. 04 Mar, 2011 1 commit
  26. 20 Feb, 2011 5 commits
  27. 19 Feb, 2011 1 commit