Recently, a ProofGeneral  package  was submitted to Fedora.
Since I had used ProofGeneral a little bit several years earlier, I
signed up to review this package. Subsequently, a couple of issues
have arisen that I think are of interest to this audience.
First, ProofGeneral contains an X-Symbol  fork. Upstream X-Symbol
appears to be dead. Therefore, the ProofGeneral maintainers have
freely made changes to a copy of X-Symbol, and ship that with their
product. The problem is that they didn't do any namespace management,
so the two versions conflict. I have not examined them yet to see if
the ProofGeneral version has altered the API. What we really need is
for someone to step up and start maintaining X-Symbol again, starting
by examining what the ProofGeneral team has done. Any volunteers?
Second, the ProofGeneral compilation succeeds on 21.5.28 and earlier,
but fails on 21.5.29 . The failure is caused by changes to the
char-table/display-table interface. Those tables used to be
represented by vectors, but are now represented by objects. The
make-display-table help suggests adding a couple of wrapper functions.
That suggestion is lacking in two ways: (a) it suggests the use of
defun-when-void, which is not available on Emacs (defun-maybe, in
APEL, is); and (b) those two functions are not sufficient to cover the
space of all manipulations that might be desirable. For example, the
ProofGeneral code does this:
(fillarray table "")
XEmacs 21.5.29 doesn't much care for that fillarray. At the very
least, we need to also suggest this:
(defun fill-display-table (value display-table)
"Make every entry in the table map to VALUE."
(if (sequencep display-table)
(fillarray display-table value)
(put-char-table t value display-table)))
... except I'm not at all sure the else branch of that conditional is
correct. If not, would a knowledgeable person please help me correct
XEmacs-Beta mailing list