GitLab

As they say, "A penny saved is ridiculous."

Note: Currently, only the set of real theories has been fully converted to
the new script format. So it is the only one enabled. The other ones would
not survive the process.

Make its building rule a bit quieter.

That should fix the build failure of the nightly bench.

Also, do not build the bytecode of the why3 library when compiling
in native code.

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

Split session in two :
Session : an API for managing session without running provers
Session_scheduler : an API for running provers asynchronously

All the global states have been removed.

A session must be first read, which give a session without task.
Afterward it must be updated to the current state of the files with
some environnement and configuration.

printer and iterator are provided for session.

Session_tools : some useful functions on session.

Smoke detector : not anymore integrated to session. Just add the
      transformation "smoke_detector_top" or "smoke_detector_deep" to
      all the valid proof attempt.

prover_id are not yet removed but all is in place in session for that.

Note that the file is still generated at compilation time.

The "realized" meta takes two arguments. The first one is the path+name of
the theory, the second one is the translation of it for the target prover.
The meta is supposed to be put into a printer file, so there is no
ambiguity on the target. The second argument can be left empty if it can be
inferred from the first one.

Note that the first argument is not really satisfactory, since it is
redundant with the theory part of the driver. Moreover, its handling is a
bit crude: it does not take into account rich qualifiers and it does not
generate proper error messages if it does not match the theory.

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.