Re: [isabelle] Two configuration questions



On Mon, 10 Feb 2014, Van Staden Stephan wrote:

I have some trouble configuring a fresh Isabelle2013-2/jedit installation:

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.


	Makarius




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