GitLab

              when one of the field is empty.

              (Thx Jean-Christophe)

(no yet displayed in IDE)

new goals are associated to old goals directly in the order they appear.
they are all marked obsolete, unless the theory itself is found non
obsolete (thanks to the new checksums for theories)

in other words, reloading a session on a file that did not change results
in non-obsolete goals, even if checksums and shapes are absent (e.g. if
the file was not put under version control)

and merge the why3 and why3session libraries back into one.

- make Whyconf.Args.initialize return the base config file, too.
  This is needed when we change configuration and want to save it.
- make Main pass "why3 <command>" as argv[0]
- remove "-version" options from everything but the main executable

two parts: why3 and why3session.

(The Coq tactic does not include why3session)

              rename options of why3session csv

	Just a proposition for a more controllable why3replayer

can be used with the task in a session

+ rename Debug.Opt to Debug.Args to avoid conflicts

+ create AUTHORS file
+ fix the linking exception in LICENSE
+ update the "About" in IDE
+ remove the trailing whitespace
+ inflate my scores at Ohloh

       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.

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