1. 04 Aug, 2012 1 commit
  2. 03 Aug, 2012 1 commit
    • François Bobot's avatar
      Documentation: add description to all the registration functions · 29201f7c
      François Bobot authored
       (metas, debug flags, transformations, formats) except for label.
      
      This description is used in --list-*. The description can use any of
      the formatting markup of Format "@ " "@[",...
      
      Transformations can also specify from which metas and labels they
      depend, and add informations about how they are interpreted.
      
      TODO:
        - complete and correct the documentation
        - when a transformation use Trans.on_meta, it should be possible to
          add an interpretation of the metas in the documentation.
        - recover a summary version of --list-* ?
        - be able to export in latex?
      29201f7c
  3. 25 Jul, 2012 1 commit
  4. 23 Jul, 2012 5 commits
    • François Bobot's avatar
    • François Bobot's avatar
      prover identification: use shortcuts · 92165a83
      François Bobot authored
         shortcuts are defined in why3.conf. They are automatically
         generated using two mechanism:
         - a shortcut section in prover-detection-data.conf creates a shortcut
         for the first prover that match the regexp
      
         - the identifier used as family argument for the prover section in
         prover-detection-data.conf is used as shortcut for the prover. If
         different sections use the same argument the first one that match an
         existing prover is used for the shortcut.
      92165a83
    • François Bobot's avatar
      new prover identification: remove id · 5a3641ec
      François Bobot authored
             Remove the id in prover that is used only for command-line, use
             instead the name,version,alternative of the prover. One can
             also use regular expression (start with ^).
      
             "Alt-Ergo,0.92,with arrays" corresponds only to one prover
             "Alt-Ergo,^0\.9.*,with arrays" correspond to all the Alt-Ergo prover with arrays which version match "0\.9.*"
             "Alt-Ergo" is the same thing than "Alt-Ergo,^,^"
             "Alt-Ergo,0.92," corresponds only to one prover with the alternate fields empty
             "Alt-Ergo,,with arrays" corresponds to "Alt-Ergo,^,with arrays" since the version is never empty.
      
             Provers identification are case sensitive even if it is
             currently more complicated for the user because
             case-insensitiveness is not sufficient. Specifiying "alt-ergo"
             for "Alt-Ergo,^,^" is great, but not if there is more than one
             match. A more general system of shortcut would be more
             appropriate.
      5a3641ec
    • François Bobot's avatar
    • François Bobot's avatar
      Autodetection: new semantic of provers-detection-data.conf · 48685ba9
      François Bobot authored
      Don't use anymore the family argument.
      
      1) For every block, for every executable call the prover using the
      version switch and add the prover to the configuration if the version
      match one of the version_ok or version_old but none of the version_bad
      2) We consider that an executable name which appears in a block, but
      which version isn't a version_ok, version_old or version_bad has an
      unknown version
      3) For every executable which have an unknown version, we add the
      prover using the first block that contains it.
      
      So the order of the block is used only when the version of an
      executable appears in none of the block.
      
      A block with more than one exec fields is now the same thing than if
      you split the block into blocks containing one field.
      
      New message field that allows to print a message when a prover is
      detected. If a message is not present, we print ", Ok." if the version
      is good (version_good) and not old, and " (it is an old version)." if
      the version is old (version_old).
      
      The field command can be missing in a block, in that case the block
      defines a version known to be buggy: no prover config is generated.
      48685ba9
  5. 20 Jul, 2012 1 commit
  6. 20 May, 2012 1 commit
  7. 09 Apr, 2012 2 commits
  8. 18 Mar, 2012 2 commits
  9. 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
  10. 15 Dec, 2011 1 commit
    • Guillaume Melquiond's avatar
      Add an --extra-config option to load additional configuration. · 5c4b2517
      Guillaume Melquiond authored
      The loaded files are slimmed down version of the standard configuration
      file. They only support the following sections and fields:
      
      [main]
        loadpath=
        plugin=
      [prover ...]
        option=
        driver=
      
      It is also possible to define brand new [prover] sections.
      
      For now, the only supported frontends are why3 and why3ide.
      5c4b2517
  11. 04 Nov, 2011 1 commit
  12. 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
  13. 01 Jul, 2011 1 commit
  14. 24 May, 2011 1 commit
  15. 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
  16. 31 Mar, 2011 1 commit
  17. 20 Feb, 2011 1 commit
  18. 19 Feb, 2011 1 commit
  19. 15 Feb, 2011 1 commit
  20. 13 Dec, 2010 1 commit
  21. 12 Nov, 2010 1 commit
  22. 26 Oct, 2010 1 commit
  23. 25 Oct, 2010 1 commit
  24. 08 Sep, 2010 1 commit
  25. 04 Sep, 2010 2 commits