Custom Query (361 matches)

Special messages, such as priority ones, but probably also tracing, are often duplicated in the output. The *isabelle* buffer contains messages only once, as expected.

This has been reported on Ubuntu with Emacs 23, but also other combinations.

This is GNU Emacs 23.2.1 on Mac OS.

Byte-compilation via make EMACS=/Applications/Emacs.app/Contents/MacOS/Emacs compile fails with strange errors like this:

coq/coq.el:291:8:Error: `save-excursion' defeated by `set-buffer'

The source in question in this case is

(defun proof-last-locked-span ()
  (save-excursion ;; didn't found a way to avoid buffer switching
    (set-buffer proof-script-buffer)
    (span-at (- (proof-unprocessed-begin) 1) 'type)
    )
  )

The same for isar, lego etc. Maybe this indicates an actual instability that was undetected so far.

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