Re: [isabelle] Isabelle2016: sledgehammer ignores prover list



Hi Christoph,

> when I write "sledgehammer" in the main Isabelle/jEdit window in
> Isabelle2016, the "output" panel shows a list of sledgehammer results,
> as expected.  However, it
> 1) lists at most as many results as the "threads" configuration says,
>   so 4 threads = 4 results

This is because the "smart" default list of provers is used, and that smart default does just that. Write

    sledgehammer_params

to see the default (under "provers =").

> 2) seems to ignore the list of provers I give to sledgehammer in the
>   Isabelle plugin configuration.
> 
> For example, the default list of provers is:
>  e z3 cvc4 spass remote_vampire

I presume you are referring to the Sledgehammer panel. The panel has its own options and lives its own life. These options only concern the "Apply" button in the panel, not the lower-level "sledgehammer" (and "sledgehammer_param") commands.

I hope this clarifies things.

Cheers,

Jasmin





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.