1. 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.
        - 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?
  2. 23 Jul, 2012 1 commit
    • 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
  3. 09 Apr, 2012 1 commit
  4. 11 Mar, 2012 1 commit
  5. 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
  6. 19 Feb, 2012 1 commit
  7. 31 Jan, 2012 1 commit
    • François Bobot's avatar
      Why3session : a new why3 program · da5b5d18
      François Bobot authored
      It's goal is to allow to view and modify sessions.
      Currently three sub-commands :
      info : can give the provers used, pretty-print in ascii a session,
           can give the corresponding directory
      mod : allow to set obsolete, or modify the archive state of proof attempt
          which corresponds to selected provers
      copy : copy a proof attempt by modifing its prover
  8. 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.
    • François Bobot's avatar
  9. 27 Dec, 2011 1 commit
  10. 15 Dec, 2011 3 commits
  11. 25 Oct, 2011 1 commit
  12. 30 Sep, 2011 2 commits
    • 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.
    • Andrei Paskevich's avatar
      rename Env.create_env_of_loadpath to Env.create_env · b92e64bc
      Andrei Paskevich authored
      also add Env.get_loadpath to use for Coq realisation
  13. 29 Sep, 2011 1 commit
  14. 27 Sep, 2011 1 commit
  15. 17 Sep, 2011 1 commit
  16. 02 Jul, 2011 2 commits
  17. 01 Jul, 2011 2 commits
  18. 30 Jun, 2011 1 commit
  19. 18 Jun, 2011 1 commit
  20. 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
  21. 24 May, 2011 1 commit
  22. 03 May, 2011 1 commit
  23. 16 Mar, 2011 1 commit
  24. 15 Mar, 2011 1 commit
  25. 20 Feb, 2011 1 commit
  26. 16 Feb, 2011 1 commit
  27. 15 Feb, 2011 1 commit
  28. 28 Jan, 2011 1 commit
  29. 27 Jan, 2011 1 commit
  30. 26 Dec, 2010 1 commit
  31. 18 Dec, 2010 1 commit
  32. 13 Dec, 2010 1 commit
  33. 10 Dec, 2010 1 commit
  34. 05 Dec, 2010 1 commit