Re: [isabelle] Isabelle2013-1-RC3: try no longer seems to give preference to try0 over sledgehammer



Hi Christoph,

Sorry for the delay in answering.

> my impression (which may have been wrong) from Isabelle2013 was that
> "try" tries "try0" before "sledgehammer".  In Isabelle2013-1-RC3 this no
> longer seems to be the case.

"try" does a number of things in parallel, using the ML function "Par_List.get_some". Because it may use several threads in parallel, there are no guarantees about which result will be printed first. Usually, "try0" results tend to be shown first because the "try0" thread is launched first and it tends to return first as well; but Sledgehammer has become faster, and "try0" is only as fast as its slowest tool (with a timeout of 5 s).

In short, this does not appear to be a deep difference between Isabelle2013-1-RC1 and Isabelle2013, but rather a matter of (bad) luck.

Still, the behavior you described is somewhat undesirable, so I've now made it less likely to happen in the repository version of Isabelle (change c7af3d651658). When "try0" is invoked from "try", it now stops as soon as it has found one proof, instead of reporting detailed timings for different tools.

Since this is not a true regression, and there is an easy workaround (i.e. invoke "try0" directly), I will not ask Makarius to add the change to the final version of Isabelle2013-1. If this is very important to you, I would suggest that you apply the patch locally. In any case, the patch should be part of (the expected) Isabelle2014.

Thank you for your report.

Regards,

Jasmin





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