Email Gateway (Aug 22 2022 at 12:38): Email Gateway (Aug 22 2022 at 12:38):From: Makarius <makarius@sketis.net>
On Wed, 10 Feb 2016, Andreas Lochbihler wrote:
Consider the following scenario in Isabelle2016-RC4:
- I run sledgehammer via the sledgehammer panel,
- One of the provers comes back with a metis proof while the others are
still running.- 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
Email Gateway (Aug 22 2022 at 12:40):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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.
Thanks,
Andreas
Email Gateway (Aug 22 2022 at 12:52):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Jasmin and Makarius,
Consider the following scenario in Isabelle2016-RC4:
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
Last updated: Nov 21 2024 at 12:39 UTC