GitLab

IDE: context menu now contains more or less the items that were in the left toolbar in former versions of Why3

The new shortcut for "copy" forces to change the one for "collapse all
proven", which is now "!". The "expand all" command has been removed,
since pressing "+" twice (i.e., double expand) now has the same effect.

This is fixed at 3/4 (random) the size of the main window

This lets us write "let ghost (x, y) = 0, 0"
instead of "let ghost x, ghost y = 0, 0".

doc modified accordingly

fixed doc

Corrected typo in Pretty.ml

On a missing "diverges", Vc emits a warning and adds
a "false" sub-goal at the location of the non-terminating
loop or function call. The explanation on this sub-goal is
"termination", but should probably be "termination (failure)".

The "diverges" clase propagates downwards: if it is put on
the top-level function, there is no need to repeat it on local
functions or abstract blocks.

The contextual menu inkoved by mouse-3 is now simplified: it contains only
the strategies and the provers that are marked visible in the preferences

For the previous behaviour (no import), write "use/clone T as T".

This shortens the most used "use/clone import" to simply "use/clone".

Clone "with axiom ." or "with goal ." to change the default
("with lemma ." is also accepted, just in case).

NoProgress is raised by apply_trans not Exit. Noprogress without
uppercase P is removed.

Some why3doc comments in the gallery contains "[i,j[", which breaks the
documentation since it opens a code block that is never closed. The proper
way to write it is "[\[i,j\[]", which is not only ugly but also
error-prone.

This commit introduces a Markdown-like syntax for embedded code. It uses
the backtick as a delimiter: "`[i,j[`". It also supports multi-backticks:
"you can delimit code using `` `...` ``".

Menhir 20151112 can, in fact, be used to compile Why3. The actual issue
was that the error reporting module depends on Menhir's table-based
backend, which requires menhirLib. So, the latter is no longer an optional
dependency.

Detect and push down the VC explanations during introduce_premises.

These names are only visible under "ensures" but not under "returns".
If the result is named, the special variable "result" is not used.
In a tuple, either each component should be named, or none at all.
Underscores are allowed. Parentheses around the return type are required.
Each name must be given its own type: "f () : (x y: int)" is rejected.
Identifiers without cast are treated as types, not as names.
To name the result without giving its type, use "returns".