proof-full-annotation causes instabilities

[Makarius]

This is GNU Emacs 23.x on Linux or Mac OS.

The default proof-full-annotation uses a lot of resources, both on the Emacs and ML side, resulting in odd instabilities.

For example, open the file Isabelle2011/src/HOL/Auth/Message.thy and assert the whole buffer. This is quite slow, and there is a good chance that it stops in the middle with an Interrupt from the prover (which indicates some low-memory situation).

For this reason, the distributed Proof General is patched to have proof-full-annotation disabled by default.

[Makarius]

The deeper reason is that the default setup runs various funny plugins as part of the state display operation. This makes it very slow, and occasionally exhibits race conditions in the dated timeout mechanism being used here.

Conclusion: do not enable for isar .

[David Aspinall]

I am surprised this causes problems inside Isabelle since it is merely based on re-enabling printing of intermediate states. I know that this affects speed of processing, and there are warnings about this in the UI and documentation.

How can these things be fixed or worked around inside Isabelle?

Early feedback from users who have tried this additional markup is that they like it.

[David Aspinall]

I've tried the file suggested now in Isabelle2011, and it works fine for me, it only takes a few seconds and seems to label the proof states fine.

Are you sure you didn't have other things switched on?

[Makarius]

There are two fundamental problems here, of different severity:

• Printing of proof states is sometimes really slow, probably for reasons of excessive user abbreviations, translations etc. (There are known examples in HOL/Bali that still need to be pinned down exactly.) So if all intermediate states are printed by default, which is inherently synchronous in PG, there is some danger that the system becomes unusable in unexpected situations. BTW, I3P users have already discovered that effect, resulting in some follow-up change in its interaction model, to make goal display more lazy. Isabelle/Scala? also includes some crude mechanism for asynchronous state output, which needs some further refinement in the future.

• More seriously, the TTY/PG setup of goal printing is piggy-backed with funny agents that report on the goal (quickcheck and the like). So full-proof-annotation enabled together with some of these "auto" gimmicks can easily lock-up or crash the prover process. You can rightly blame the Isabelle setup for that, but it has been fabricated some years ago under certain assumptions how PG uses disable_pr and enable_pr to make it work more than half-way. With full-proof-annotation these assumptions no longer hold.

[David Aspinall]

Thanks for the elaboration... the second case sounds bad, can you give a concrete example test case to demonstrate? A work-around in the interface might be to prevent enabling the auto checks when full annotation is on.

[David Aspinall]

Still no further information or concrete examples, bumping to 4.2. Usefully/obnoxiously, leaving this setting enabled by default may help us find some examples and see if we can repair them, while PG/TTY interaction is still enabled. Alternatively, if PG can issue a command to inspect the previous state upon mouse hovers, we could use that feature instead.

[David Aspinall]

Closing this as there is nothing that can be fixed in Proof General to repair the problem (short of introducing lazy asynchronous state querying). The default for proof-full-annotation is now nil anyway.