Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Proof General on FC6


view this post on Zulip Email Gateway (Aug 18 2022 at 10:00):

From: David Aspinall <David.Aspinall@ed.ac.uk>
Hi Gergely,

You have a plausible combination of versions. It seems like you see a
low-level XEmacs crash maybe caused by using old binaries with the newer
distribution. You could try rebuilding from the source on FC6 ---
please let us know how you get on if so.

Alternatively, the beta-stamped version of XEmacs that FC6 has thrust on
us can be made to work with the current CVS/development version of PG
(which should still supports Isabelle 2005 in Isar mode), but you may
hit nasty errors with X-Symbol/character encodings if you start it with
the "Isabelle" script. At least, this is what I see using Isabelle CVS,
I'm not sure about Isabelle2005. Starting XEmacs first avoids some of
this (see ProofGeneral/INSTALL) but may not set the environment
variables exactly the way that Isabelle likes them -- and leaves odd
characters in the output. I hope to fix this last problem soon.

I'm sorry for these troubles, but maintaining forward and backward
compatibility across Emacs and prover versions is near impossible, we do
the best we can.

- David.

Gergely Buday wrote:


Last updated: May 03 2024 at 12:27 UTC