A new version of proof-general has been released. The 4.0 ebuild works unchanged with the new version.
Unfortunately, byte-compilation fails with the latest Emacs 24 pretest (emacs-vcs-24.0.90): emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/var/tmp/portage/app-emacs/proofgeneral-4.1/work/ProofGeneral-4.1/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego pgshell phox generic lib ))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn t))' -f batch-byte-compile isar/isabelle-system.el In toplevel form: isar/isabelle-system.el:295:16:Error: `interactive-p' is an obsolete function (as of Emacs 23.2); use `called-interactively-p' instead. make[1]: *** [isar/isabelle-system.elc] Error 1 make[1]: Leaving directory `/var/tmp/portage/app-emacs/proofgeneral-4.1/work/ProofGeneral-4.1' make: *** [compile] Error 2 emake failed I'd rather like to have this problem fixed before doing the version bump. Could you report it upstream please?
This should be fixed in the latest prerelease. The patch is http://lists.inf.ed.ac.uk/pipermail/proofgeneral-devel/2011/000202.html
proofgeneral-4.1 committed to CVS, sorry for the delay. Thank you for the patch.