On Tue, Jul 7, 2009 at 5:59 AM, Stephen J. Turnbull<stephen(a)xemacs.org> wrote:
ProofGeneral is an Emacs-based (IIRC) front-end for several proof
assistants. It would enter as a package. AFAICS, there's no
particular need for it to be restricted to XEmacs 21.5.
My primary concern right now is to beat it into shape so it can enter
Fedora. I suppose we could look into adding it into our package set.
Frankly, the community that uses it is both small and highly
specialized. I don't know that we would be helping all that much by
making it an official package.
For the same reason that LaTeX users want them: you can get the
glyphs for Greek letters, logical quantifiers, and operators, instead
of using some verbose transliteration.
Yes. It turns out that the problems I raised were punted by some
other distributions. Debian, for example, builds ProofGeneral without
its X-Symbol support, thereby dodging the associated problems.
One question I'll try to get answered right away is whether upstream
is truly dead or just dormant. I'll let you know if I get any
XEmacs-Beta mailing list