proof-process-buffer very slow

[Makarius]

GMU Emacs 23.1.1, Mac OS.

Asserting a whole buffer via proof-process-buffer is very slow. One can watch the frontier of the locked region move in slow-motion. This is a MacPro? with 2.8 GHz and 8/16 cores (of course Emacs can use only 1 core anyway).

[David Aspinall]

Thanks for raising, this does need improvement. I have noticed also on Linux but haven't probed deeply yet.

I suspect there are at least a couple of sources of the delay: (1) unicode tokens, which takes the Emacs display engine hard and (2) "full annotation" which is recording the output of commands inside the script. You can turn both off inside the menu Proof-General -> Options. Does that lead to the speed you expect?

[David Aspinall]

The main reason turned out to be an experiment with `process-adaptive-read-buffering', setting it to adapt to longer delays in output but not shrink the delay down again (the clue was in CPU usage which showed waiting somewhere). That setting was clearly wrong: it might be that the ordinary adapting read may be better than no adaptation, that needs some more experimentation.