Email Gateway (Aug 22 2022 at 09:52): Email Gateway (Aug 22 2022 at 09:52):From: Peter Lammich <lammich@in.tum.de>
When sledgehammer runs in the background (invoked via the panel),
the output of commands that I enter is not displayed in the output
panel, until sledgehammer terminates.
A very annoying behaviour, if you want to continue exploring your proof
while sledgehammer tries to find a "shortcut" for you.
-- Peter
p.s. I also reported this problem for Isabelle2014.
Email Gateway (Aug 22 2022 at 09:52):From: Makarius <makarius@sketis.net>
Can you be more specific about the situation, especially the number of
cores and ML threads, and sledgehammer provers?
For Isabelle2015 the scheduling has changed, to address that particular
shortcoming of earlier versions. It now works quite differently from
Isabelle2014.
In the tests I've made myself, it did work as intended. It was also
occasionally discussed on various Isabelle2015-RC threads on the mailing
list, where I called explicitly to test it thoroughly and produce tangible
problem reports.
Makarius
Email Gateway (Aug 22 2022 at 09:53):From: Peter Lammich <lammich@in.tum.de>
Can you be more specific about the situation, especially the number of
cores and ML threads, and sledgehammer provers?
How to find out this information?
I have an "Intel(R) Core(TM) i7-4810MQ CPU @ 2.80GHz" with 8 (virtual)
cores with 16GiB RAM running an Ubuntu 14.04.
I changed nothing in the Isabelle configuration that came with RC5. I
have no idea how to find out/change the number of ML-threads.
The provers text field says: "cvc4 remote_vampire z3 spass e",
isar-proofs is not checked, try methods is checked.
If I start Isabelle from the console, I get a message
C/C++)
although I have the libc6-i386 package installed.
Last updated: Apr 25 2024 at 12:23 UTC