Re: [isabelle] [Isabelle2016-RC4] sledgehammer blocks metis proofs
On Wed, 10 Feb 2016, Andreas Lochbihler wrote:
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
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?
Note that priorities don't help, when all worker threads are already busy
working on tasks. So the usual working hypothesis is that sledgehammer is
already saturating all threads, and the PIDE execution task (after an
edit) is still waiting in the queue.
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
This hardware provides 4 active worker threads by default.
I have experimented a bit with threads=4 and
bigo_elt_subset (after the "rule_tac" and before the "metis"), both in
Isabelle2015 and Isabelle2016-RC4.
After pushing the Sledgehammer button, I waited for the first result and
copied that into the text:
apply (smt less_imp_le less_le_trans mult.assoc mult.commute
mult_less_cancel_right not_less zero_less_mult_iff)
Later I also let Sledgehammer provers run and just copied the same text to
see what happens.
This uniformly leads to a "pink" (i.e. queued, not yet evaluated) 'apply'
command. Both for Isabelle2015 and Isabelle2016-RC4.
The key difference: Isabelle2015 with default configuration immediately
says: "remote_vampire": Error: SystemOnTPTP is not available. In that
situation, the 'apply' line was checked earlier, probably because one
thread became free on time to continue the PIDE execution.
In Isabelle2015 with proper remote_vampire, I've seen the unchecked pink
In all situations with threads=6, I see immediate checking of the 'apply'
So unless there is a clear indication that something changed to the worse,
I would say it is the normal state of affairs.
BTW, with 4 cores and hyperthreading you could experiment with threads=5
or threads=6; threads=8 will probably make the machine very hot without
This archive was generated by a fusion of
Pipermail (Mailman edition) and