#779 No information when failing to launch external provers

[Nicolas Beauger]

When an external prover cannot be launched, the UI only shows "Failed" in the notification area at the bottom, just as if the prover had been launched but could not prove the PO. The error log contains nothing about the failure.
This case must be handled with more precision so as to avoid confusion or the impression that it "just doesn't work":

• show a popup (with a "don't show again" option) which clearly states the launch failure.
• whenever possible, indicate the cause of the failure

The known causes of failures are:

• file system errors (file does not exist, restricted permission)
• missing system library

A common case of missing system library is related to 32 bit binaries (like the Atelier B provers or some of the SMT provers) on 64 bit Linux OSes, where a 32bit compatibility package is required. The package is named 'libc6-amd64:i386' in Ubuntu and Debian repositories. Although this information is given in the release notes, not all of the users are aware of it and Rodin should remind about it in such cases.

[Laurent Voisin]

The current infrastructure for running external provers does not allow to implement a fix directly. The error message returned by the tactic of the external prover gets mangled by the tactic loop .

I see two options:
either the tactic loop gathers all messages from failed sub-tactics and returns it.
or we implement a global UI command for running the external provers on a trivial sequent to chek that they work properly.
The second option would allow to print a proper message in case an external prover does not work.

[Laurent Voisin]

After discussion with Nicolas, the plan is to implement a check at the UI startup. This check takes each contributed tactic from an external plugin and attempts to run it on a trivial sequent. If the tactic fails, the returned message is displayed to the user. To avoid repeating this check at every startup, a workspace preference is used to remember each tactic known to work (and the associated plug-in version), so that it is not checked again. A new command would allow to erase this memory and rerun all checks.

[Laurent Voisin]

Implemented in [2c0f5f]: run a check (with cache) at startup and provide an interactive command to run it manually (from the Run menu).