GitLab

Even when checksums are equal, we check that the shape are oks. This
allows to keep examples with up to date shape.

The code in file /src/util/pqueue.ml has been extracted from a Why3 proof,
and is now a correct-by-construction OCaml code. This file depends on the Vector
module, which is also an OCaml implementation extracted from another Why3 proof.
The proofs can be found in /examples/util/

This is the result of Aymeric Walch bachelor internship.

- 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)

- requires a lot more testing
- support in extraction missing (exception raised)
- interaction with "syntax literal" remains to investigate

* declare range types and float types,
* use integer (resp. real) literals for those types through casting,
* specify how to print them in drivers.

Change in syntax
* use

  type t = < range 1 2 >   (* integers from 1 to 2 *)
  type t' = < float 4 12 > (* float with 4 bits in exponent and 12 in mantissa *)

  the two projections :
  t'int
  t''real

  and the predicate :
  t''isFinite

* Restrict the use of "'" in whyml:
  Users are not allowed to introduce names where a quote symbol
  is followed by a letter. Thus, the following identifiers are
  valid:

  t'
  toto'0''
  toto'_phi

  whereas toto'phi is not.

Note: we do not yet support negative numbers in range declaration
and casting of a literal.

also, rename asym_label to asym_split and keep_on_simp_label
to keep_on_simp.

So that it can be used to search for other labels.

* termcode.ml
(search_labels): basically a copy of get_expls_fmla with extra argument
for the callback
(get_expls_fmla): rewritten to use search_labels

So that it can be used to search for other labels.

* termcode.ml
(search_labels): basically a copy of get_expls_fmla with extra argument
for the callback
(get_expls_fmla): rewritten to use search_labels

up to this point, we used Clone declarations with an empty substitution
to represent use of theories in tasks. The intention was to stress the
fact that the imported declarations are physically present in the task
and thus are followed by a "witness" Clone declaration (whereas a Use
inside a theory acts rather as a pointer to follow).

However, this encoding requires the clone substitution to cover every
locally defined symbol: otherwise we might not be able to distinguish
a use from a clone. Therefore, we had to clone even Pgoal propositions
as Pskip, in order to keep the substitutions complete.

This commit restricts the Clone declarations in tasks to actual
theory cloning, and represents theory use with Use declarations.
This hopefully makes the API more clear, and will allow us to
abolish Pskip.

http://linuxtesting.org/astraver)

(no yet displayed in IDE)

new goals are associated to old goals directly in the order they appear.
they are all marked obsolete, unless the theory itself is found non
obsolete (thanks to the new checksums for theories)

in other words, reloading a session on a file that did not change results
in non-obsolete goals, even if checksums and shapes are absent (e.g. if
the file was not put under version control)

and merge the why3 and why3session libraries back into one.

two parts: why3 and why3session.

(The Coq tactic does not include why3session)