Re: [isabelle] »strict« or »sequential« mode in Isabelle/jEdit?
On Sun, 13 Apr 2014, Florian Haftmann wrote:
* If existing proofs degenerate into non-termination, the risk is that
these spots will consume a lot of resources and turn Isabelle/jEdit
little reactive until the spots are identified and interrupted by hard
What works as workaround is to set the number of threads temporarily to
1. Beside the comparably deep path through GUI elements for switching
back and forth, parallelism (e.g. wrt. complete theories) is entirely
The deep path through the GUI can be avoided by mapping the jEdit action
"plugin-options" to some key that is still free on your keyboard. That
depends on many individual side-conditions and it is common practice for
jEdit plugins to provide default key bindings rarely.
In the above situation you could keep multi-threading and merely say
parallel_proofs = 0.
For further find-tuning, I need more information about your hardware and
operating system. I usually try myself on 3 quite dissimilar machines, in
the range of 2..8 cores.
Smoothness and reactivity are not automatic, but the result of adjusting
many parameters. I hope that more and more of this will get proper
defaults, but modern hardware is difficult to handle.
This archive was generated by a fusion of
Pipermail (Mailman edition) and