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 edits.

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 lost.

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 MHonArc.