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


	Makarius





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