Script management very slow on some platforms

[Makarius]

Script management seems to be quite slow on some platforms / Emacs versions. The following timings are without "Full annotations" (because intermediate goal state output can slowdown things even more), and without byte-compilation.

Here are some timings for etc/isar/AHundredTheorems.thy that are really slow:

Mac OS X, Aquamacs 2.0: 15 seconds

Mac OS X, GNU Emacs 23.1.1 or 23.2.1 ("no-nonsense" version): 10s

Cygwin 1.7.5, GNU Emacs 23.2.1: 20s

The following ones can count as "reasonably fast":

Mac OS X, Aquamacs 1.9: 3.7s

Ubuntu 10.04, GNU Emacs 23.1.1: 2.5s

BTW, Isabelle/jEdit reports the following: 0.263s elapsed time, 0.309s cpu time (of course this is a bit unfair, because that system processes things completely differently).

[David Aspinall]

Would be useful to know more, e.g., have some profiling information from these platforms and experiment with the basic IO settings for process communication which were the culprit last time we found a performance issue. The longer times suggest some bad waiting somewhere, esp if you don't see full CPU utilisation even for one core and things are not improved by byte compilation. But they might also be caused by the display engine on those strange platforms.

You can guess which platform I'm developing on, 8-).

Where is the jEdit measurement taken, is it the same everywhere? Probably even Eclipse beats 10 seconds on this test.

[Makarius]

IIRC, the jEdit timing was on the same machine as the other "Mac OS X" measurements above.

The reason why I've called it unfair is that the parsing is not included here (both "span" parsing within the editor and "Isar outer syntax" parsing). Apart from distorting measurements as seen here, it actually pays off to the user, despite inaccurate numbers. (Even more performance improvements will come after the one or two more refinements of the protocol. In particular, both parsing and printing of state output will be fully asynchronous next time.)

Anyway, back to Emacs 23: Right now PG 4 is only unusable on the usual Linux boxes.

[David Aspinall]

There is now a mechanism for testing and profiling triggered by "make profile.isar". I'd be grateful for postings of the contents of the profile output on different platforms, that might give a hint whether some Emacs function is behaving differently on a different platform/implementation for some reason.

Also, measurements are missing for Ubunutu with Emacs 23.2 (which I can probably do) or Cygwin with Emacs 23.1 (which I probably can't).

Which version is Aqua Emacs 20.0 based on? I remember when I tried it years ago there were various problems.

[Makarius]

Just rediscovered #308 -- process-adapative-read-buffering appears to be t on all these Emacsen.

[Makarius]

Aquamacs 2.0 is based on GNU Emacs 23.2.1.

[Makarius]

The above profiles have been produced on the same generous 8 core Mac Pro, but some running in Parallels VM.

[Makarius]

one more from my 2-core MacBook Pro

[David Aspinall]

Many thanks for posting these measurements. The aquaemacs 1.9 would be interesting as well, because it would allow to see some difference on the same platform.

Most of the time is allocated to proof-shell-wait, which has a call to accept-process-input that we could investigate further (e.g., reducing the timeout, adding additional parameters).

[David Aspinall]

Investigating now on OS X. I have reduced the delay in proof-shell-wait which gives much better timings on the profiling now (down to 2-3 seconds on my machine), but interactive is still slow on a brand new MacBook compared with a 3 year old Linux laptop.

Visit AHundredTheorems.thy and contrast

   M-x eval RET (proof-process-buffer) RET

with

   M-x eval RET (progn (proof-process-buffer) (proof-shell-wait)) RET

It seems likely then that the reason is caused by the Emacs top-level command loop, perhaps it is more eagerly processing sub-process output on Linux than on Mac/Windows? who favour waiting instead? Profiling doesn't show up much difference in function timings within PG for the two runs above. Changing process-adaptive-read-buffering to nil has minimal effect.

This deserves more investigation and probably bug reporting to Emacs developers, but I'm timing out on this for now.

Aside: surprising that the Aquamacs profiling runs completely headless! Only seems to display the window if input is required of user. Otherwise performance in PG seems similar to the no-sense port.

[David Aspinall]

Unlikely that changes in PG code are possible to improve this. Keeping alive as a note to investigate with Emacs developers.

Meanwhile, I have added a partial work-around with (yet another) user option: selecting Fast Process Buffer, PG will use proof-shell-wait as above, which has been changed not to display refreshes in latest CVS.

On these Mac ports this results in much faster processing of commands than proof-process-buffer because it runs a loop that polls for prover output, rather than relying on Emacs top level command loop to do this. On Linux there is an improvement of 10% or so. Probably the option should only be revealed on Mac (and Windows?).

The option only affects this one command, although it could easily be added to proof-goto-point as well.

Feedback appreciated.

[David Aspinall]

Closing this, as no further feedback or complaints received. The outstanding action in #381.