[isabelle] [Isabelle2016-RC4] sledgehammer blocks metis proofs



Dear Jasmin and Makarius,

Consider the following scenario in Isabelle2016-RC4:

1. I run sledgehammer via the sledgehammer panel,
2. One of the provers comes back with a metis proof while the others are still running.
3. I click on the metis proof which gets inserted into the main text area.

The metis proof is not run until all other provers have finished or I manually cancel them. In Isabelle2015, metis used to check while the other provers are still working. Is there any setting to prioritize Isabelle proof methods over sledgehammer provers?

Some configuration data:

List of provers: cvc4 z3 spass e remote_vampire
Try methods checkbox in Sledgehammer panel: enabled
System: Ubuntu 14.04 LTS
Hardware: Intel(R) Core(TM) i7-3630QM CPU @ 2.40GHz, 16GB RAM

Best,
Andreas




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