Common options are read twice
The common options, as declared in Whyconf.Args.common_options
, are interpreted twice, once by the main executable (see src/tools/main.ml
, line 18, options_list
contains Args.common_options
) and then again by each subcommands, typically via call to Whyconf.Args.initialize
(for example, why3 prove
, in src/tools/why3prove.ml
, line 203).
Among these common options, only two are say "cumulative": -L
and --extra-config
, they can be given several times and they are interpreted as a list.
That means that when one types say why3 prove -L . <...>
, .
is added once on the loadpath, but with why3 -L . prove <...>
it is added twice.
The fact that elements in the loadpath are duplicated is not a problem because when creating the environment, the code uses Sstr.of_list
(line 43 of src/core/env.ml
) so duplications are removed.
The fact that extra config files are duplicated is more problematic, though the current code in src/driver/whyconf.ml
is quite defensive against duplication. The only visible effect I was able to obtain is as follows : first create an extra config file myextra.conf
[prover]
name = "Z3"
version = "4.8.10"
alternative = "myalt"
shortcut = "z3alt"
driver = "z3_471"
command = "z3-4.8.10 -smt2 -T:%t sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 -st %f"
command_steps = "z3-4.8.10 -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 -st rlimit=%S %f"
then run an example say using
why3 --extra-config myextra.conf prove examples/isqrt.mlw
and one obtains
Shortcut z3alt appears twice in the configuration file
If I remove the shortcut from the config, everything is fine. I believe this is because the code in src/driver/whyconf.ml
, function Rc_load.load_prover
lines 334-382, takes into account the case when a prover is already present. But it does not handle the shortcuts, which are treated elsewhere.
Of course, a workaround would to avoid the error on the duplicated shortcut, but I believe reading twice the options is the original issue there.