Why3 must be configured to access external provers. Typically, this is done by either running this tool or using the menu File/Detect provers of the IDE. This must be redone each time a new prover is installed.
The provers Why3 attempts to detect are described in the human-readable file /usr/share/why3/provers-detection-data.conf. Advanced users may try to modify this file to add support for detection of other provers.
The result of provers detection is stored in the user's configuration file (~/.why3.conf). This file is also human-readable, and advanced users may modify it to experiment with different ways of calling provers, e.g., different versions of the same prover, or with different options.
If the user's configuration file is already present, why3config will only reset unset variables to default values, but will not try to detect provers. The option -detect-provers should be used to force Why3 to detect again the available provers and to replace them in the configuration file. The option -detect-plugins will do the same for plugins.
- -C, --config <file>
The configuration file to create.
Search for provers in $PATH.
Search for plugins in the default library directory.
Search for both provers and plugins.
Install a plugin to the actual library directory.
Do not modify the configuration file.
List known debug flags.
Set all debug flags except parse_only and type_only.
- --debug <flag>
Set a debug flag.
Print version information.
- -help, --help
Show a list of options.
why(1), why3-cpulimit(1), why3bench(1), why3doc(1), why3ide(1), why3ml(1), why3realize(1), why3replayer(1)
why3(1), why3bench(1), why3-cpulimit(1), why3doc(1), why3ide(1), why3ml(1), why3realize(1), why3replayer(1).