Re: [isabelle] Tab completion slow in Isabelle2014-RC2

On Wed, 6 Aug 2014, bnord wrote:

When typing fast and using tab completion in Isabelle204-RC2 I often end up with e.g. "sle<tab>" instead of "sledgehammer" when the system is under some load. In 2013-2 no matter how hard I try I always get the completion. I believe that I have changed all relevant settings to intermediate/0.

You probably mean "immediate". I think you also need to switch off the option "Completion Context" -- thus you are back to old-style syntactic completion, independently of prover markup (which might get delayed and thus cause non-determinism).

Instead of such a nostalgic mode that imitates old versions of Isabelle/jEdit, I recommend to study the Isabelle/jEdit manual section "3.5 Completion" and practice a little with the new defaults, which were made for mixed syntactic / semantic completion.

To improve determinism on very light machines under load it might also help to switch off the main "Completion" option and use the explicit key sequence C+b instead.

For sledgehammer in particular, the canonical way is to use the Sledgehammer panel instead of inserting a command.


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