GitLab

Term generic compare

See merge request !401

Don't crash when a syntax error occurs in MLCFG

See merge request !404

Fix datarace during the generation of version-specific realizations (fix #503).

Closes #503

See merge request !406

The same issue exists for Coq realizations, but since there are no
version-specific realizations for Coq, it never triggered. Nonetheless,
this commit also fixes it.

Minor documentation fixes

Closes #510

See merge request !405

This commit depends on a future release of Sphinx.

Compile Why3 tools as plugins (fix #485, #478, #507)

Closes #507, #478, and #485

See merge request !400

In particular, it is called lablgtk3.sourceview3 on Debian stable.

This is needed to build the IDE.

This makes it possible to launch why3ide in bytecode mode.

Since .o files are not stored inside .cma files, they are a bit difficult to
handle in a setting where tools are dynamically loaded. Hopefully, this hack is
no longer needed with recent versions of lablgtk.

When trying to edit a proof attempt for a non-installed prover, the IDE
would incorrectly complain that "for edition you must select a proof
attempt node".

Instead of crashing the IDE to the command line, let it print an error
and load the file anyways. This is the same issue as #497.

(and fix support for PVS: the load path for PVS realizations
was not the right one)

Improve handling of long options

See merge request !403

As a side effect, this fixes auto-completion for the --apply-transform
option, as the output of 'why3 --list-transforms' can now be parsed.

In particular, this commit various issues with the handling of long options.

This makes argument parsing a bit closer to GNU Getopt.

Equal is still mandatory before the optional argument of a long option.

Make IDE use native modifiers for shortcuts

See merge request !399

Improve CE model parsing

See merge request !396