GitLab

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.

Note that this is just a consequence of symbols not being imported from
realizations. If Coq files were generated with "Require Import" directives
rather than just "Require", the change would have been completely
transparent. This is not reason enough to switch to "Require Import" but
it should be kept in mind.

My first idea was to use "-R @libdir@/coq", or some other variable I would
have defined in configure.in, but it didn't work at all. Indeed, such path
variables depend on cascaded substitution, which work fine inside
make files and shell scripts, but not at all inside Why3 config files.
Note that this is a documented feature of Autoconf so I doubt there is any
way to circumvent it.

So I ended up adding a new format specifier inside call_provers: %l is
substituted by Config.libdir.

There are hardly any change to the code. It now just looks whether
dependencies are marked as realized. The old no-realization mode is
equivalent to marking no theory as realized, while the old realization
mode amounts to marking all of the theories as realized. Now, the finer
granularity make any intermediate state reachable. This is just a proof
of concept, so the actual set of realized theories is hard-coded.

The old code was assuming that, if lablgtk2 and ocamlfind were installed,
lablgtksourceview2 was installed too. The new code explicitly checks for
both libraries.

Presumably, it won't work correctly if someone has decided to install
lablgtksourceview2 in a different location from lablgtk2, but it wouldn't
have worked with the previous version either, so it isn't a regression.

This allows to call editors from IDE in a less hackish way
and might even fix the problem with Coq editing on Windows.

Suppose that marks appear in order L1, L2, L3 in a program.
Previously, x@L2@L1@L3 would end up with the value of x at mark L1 (the latest mark encountered by WP, that is, the earliest mark in the program).
Now, x@L2@L1@L3 will end up with the value of x at mark L2 (the innermost mark in the expression).

From a WP point of view, the sequence was
x@L2@L1@L3 -> x@L2@L1@now (L3) -> x@L2@L1 (unref) -> x@now@L1 (L2) -> x@now@L1 (unref) -> x@now@now (L1) -> x_L1 (unref).
Now the sequence of substitution is
x@L2@L1@L3 -> x@L2@L1@now (L3) -> x@L2@L1 (unref) -> x@now@L1 (L2) -> x_L2 (unref).

the memlimit parameter is ignored and the timelimit parameter
is still treated as a wallclock time. However, the execution
time shown is the CPU time.

This is only a draft which may not even compile.

Circumvent problem with implicits

the time limit for the replay is the max of the time limit
given initially and twice the time taken by the prover
(if the result was "valid")

E.g, if Alt-Ergo said valid in 4.9 seconds, for an initial limit of 5,
then the replay will give 10 seconds