Do not update the proof duration if it changed by less than 10% or 0.1s, so as to avoid diff noise in session files.

The only significant difference between these functions is that the first
one is calling a callback function at each step, while the second one is
generating a report at the end. Any other differences are likely to be
actual bugs, which hopefully are now fixed. Now both functions call a
third one, which accepts callbacks that encompass all the previous
features.

Disclaimer: the code is ugly.

allows to show the warnings in the nightly bench

If the user happens to select all the goals in the IDE and press replay,
a quadratic number of proof attempts are actually scheduled: each goal is
scheduled as many times as it has ancestors. This patch fixes it.

With the previous code, one could start with an original time limit of a
few seconds and end up with proof attempts running for several minutes
after a few unsuccessful tries with provers that are aware of the actual
limit. Now, the actual time limit is never more than twice the user-defined
one.

  - the symbols that appear in the metas are identified in the xml by
    their position in the task:
    - in which declaration
    - in which definition (if that apply otherwise -1)
    - in which constructor(or case in inductive predicate) (if that apply otherwise -1)
    - in which field (if that apply otherwise -1)

  - the md5sum of the prefix of the task that end with the declaration is used to know if the
    symbol have been changed, and if it is obsolete.

  - currently metas that contains obsolete symbol are removed.

and Debug.register_stop_flag into register_flag. While information
flags (selectable by --debug-all) are more common, it is safer to
treat a generic debug flag as behaviour-changing by default.

comportement was not very clear if an exception was raised.

 (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?

the original file is properly saved and restored upon completion
(whatever the result is)

warning: the behavior regarding edited files is still not the one in
the doc: the proof script should be copied, instead of empty

Among other things, a missing editor now displays a bomb in the left pane
and an exit status 127 in the right pane. While it is not as user-friendly
as it could be, it gives at least some visual feedback now.

There is still a need to have some proof replacement process

For now, there is no autodetection of the editor. The purpose of this patch
is only to provide the user with sane defaults and to avoid reusing prover
options as editor options. So the user has to manually edit the why3.conf
file to modify a prover/editor association.

Tested with Coqide 8.3 and Proof General 4.1.

when replaying proofs.

Fix : if the session points to an edited file that doesn't exist do as if the proof attempt is not edited

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