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

Hi Makarius,

You are right. With threads=5, the metis proof is being processed while the other provers are still running. So this was really just a coincidence that Isabelle2015 has one thread available for processing.


On 12/02/16 17:34, Makarius wrote:
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 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?

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
~~/src/HOL/Metis_Examples/Big_O.thy: lemma 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 'apply' again.

In all situations with threads=6, I see immediate checking of the 'apply' line.

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 much benefit.


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