Re: [isabelle] Two configuration questions
On Mon, 10 Feb 2014, Van Staden Stephan wrote:
I have some trouble configuring a fresh Isabelle2013-2/jedit
1. It seems that sledgehammer only invokes "e" and "spass".
That actually depends on your number of Isabelle/ML worker threads, which
is determined from the number of harware cores.
Sledgehammer has some builtin smartness to guess which provers you want.
But that is not immediately obvious, and based on assumptions from TTY /
Proof General interaction, where the ML process is idle waiting to process
the next command, and then has all cores available. These assumptions no
longer hold in Isabelle/jEdit, where many things can run in parallel all
the time --- which was the whole point of the exercise to go beyond TTY /
Proof General several years ago.
Sledgehammer defaults need to be sorted out again for the next release
(summer 2014), to make it clear and simple what the configuration is, and
where it is actually configured.
Until then, you can write the list of provers for Sledgehammer into the
"Provers" entry field in the Isabelle/jEdit Sledgehammer panel. Then type
RETURN to run it and make that content persistent in the history of the
text field. Next time, the field content will default again to the
dynamic smart value provided by Sledeghammer from Isabelle/ML, but you can
select an alternative from your GUI history, using the triangle or
right-click on the field as usual in jEdit.
This archive was generated by a fusion of
Pipermail (Mailman edition) and