GitLab

In particular, this multiplication should avoid min/max on possibly Nan
floating point numbers: it avoids multiplication of 0 by inf.

After 11f28a8a, why3ide would not reload dependency libraries when
reloading a file. This implements 2 modes for reload_files:
- reload with libraries and drivers (intended for IDEs and graphical
interfaces)
- reload only the current file (intended to optimize Why3 used in scripts
files)

This adds an optional dependency on MPFR to run why3execute for floats. It
is also used for reals (represented as intervals of floats).
This commit does the following changes:
- update the configure/Makefile to allow MPFR dependency
- adds a MPFR wrapper so that why3execute can still be compiled if MPFR is
  not installed. In this case, an exception is raised when executing on
  real/float.
- some updates are made to the standard library so that real/float
  functions are part of the program world (and can be executed).
- pinterp changes to make elementary functions from real and float
  executable.
- add some tests under bench/interp for manual testing of this feature

Note that the correctness of the results given for reals depends on the
precision. A too low precision may give unexpected results.

Issue 371 ide slow syntax erros

Closes #371

See merge request !213

Powm extraction

See merge request !212

wmp: modular exponentiation proof

See merge request !210

adapt microc and python plugin to Ptree constructors (3d86e1c5)

See merge request !209

extends Ptree/Typing API to the entire mlw file

See merge request !199

Distinguish between "foo (): type" and "foo (): (_:type)" (fixes #360).

Closes #360

See merge request !208

Make sure that term comparison takes locations into account (fixes #366).

Closes #366

See merge request !207

The former is syntactic sugar for "foo (): (result:type)". But there is no
good reason for the latter to also be syntactic sugar for it.

All the changes are due to equality "x = x" now being properly detected
as being trivially true.

This makes t_equal_nt_na redundant. Functions t_compare and t_hash are
changed accordingly. Modules Hterm, Sterm, and Mterm are changed too.
Strict functions and modules are introduced: t_equal_strict,
t_compare_strict, t_hash_strict, Hterm_strict, Sterm_strict, Mterm_strict.

Most of the calls to t_equal (and similarly for other symbols) are kept
unchanged, which means that transformations are now a lot more lenient
with respect to equality. Only hashconsing of declarations is made to use
the strict symbols.

Clean trywhy3 a bit

See merge request !206

This avoids some idiotic warning messages during compilation:

warning: overriding primitive "caml_ephe_key_offset"
  old: .../lib/js_of_ocaml-compiler/weak.js:25
  new: .../lib/js_of_ocaml-compiler/weak.js:25