prover shortcuts: the shortcuts information can be in the prover section in order to reduce the number of section in why3.conf

   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.

       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.

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

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.

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

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.

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.

Moreover,
- Coq realizations are disabled for Coq < 8.3 due to coqdep bugs,
- Whyconf.magicnumber is incremented to ensure coqc and coqide are called
  with -R,
- realizations for FP arithmetic are disabled if Flocq is missing.

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.

Warning since 7efae3f8 yices doesn't
work with real since in assoc_mul_div a variable is the denominator.
Yices refuse that.

instead of $libdir/plugins. We have no other binary components.

	 of a file into a driver

include "toto.drv.import"

rebuild provers-data-conf when necessary; support for Gappa 0.14.0 (but Gappa's driver still to be fixed)