GitLab

Conflicts:
	examples/dijkstra/why3session.xml
	examples/dijkstra/why3shapes.gz
	src/ide/gmain.ml
	src/session/session.ml
	src/session/session.mli
	src/session/session_scheduler.ml
	src/tools/why3replay.ml
	src/why3session/why3session_copy.ml
	src/why3session/why3session_csv.ml
	src/why3session/why3session_info.ml
	src/why3session/why3session_lib.ml

On N127-001, an optimisation of the fast WP was introduced, based on
marking states that contain variables that need to be refreshed when
merging them. However, this "marked" status was incorrectly reset to
false when merging states, even though some of those "unfresh" variables
could survive the merge. The consequence was that the WP was reusing
variables too aggressively, which would result in incorrect VCs.

We now compute the marked status of a merged state from the states to be
merged: if one of them is marked, the merged state is marked too.

mlw_wp.ml:
(merge): synthetize marked status from input states

Change-Id: Ifb02c54fca58137c31762469e48b59e7c907b995

- most important improvement : the explanation, used as first part
  of the shape was computed twice ! (at least)
- several improvements in the implementation, avoid using Format
  in particular (done also in checksum computations)
- possible further improvements:
    do not compute shapes if checksums are OK
       (they must be the same as in previous session)
    do not compute goal checksums if theory checksum is OK
       (they must be the same as in previous session)

situation when Gtk is not properly loaded.

files session.ml{i}, session_scheduler.ml{i} and gmain.ml
are finally removed.

supported options of 'why3 session info: --stats, --graph, --provers
not supported: --tree, --edited-files, --dir

remove_list [H1,H2] works. Without spaces and with this exact syntax.
This is to be modified later. In particular, we should probably handle
parsing of arguments differently.

Conflicts:
	examples/dijkstra/why3session.xml
	examples/dijkstra/why3shapes.gz
	src/tools/why3prove.ml

If drivers in why3.conf are simple names like "alt_ergo", then the driver file
is search as <datadir>/drivers/alt_ergo.drv

This behavior is now the same as when a driver is given with option -D on the
command line for why3prove, why3replay or why3extract

Reminder: the datadir is either given as
1) the environment variable WHY3DATA
2) the field "datadir" of the [main] section of the
   why3 config file if exists
3) or by default the compile-time datadir

Behaviour may change in future commits.

Unfinished work to retrieve manual proofs.
(minor) added a use case for stack_trace