Re: [isabelle] Proof General on FC6

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:

I have a Fedora core 6. I've installed the following packages:

Isabelle 2005

and ProofGeneral crashes. Actually the proof general logo appears and

What is a known combination of packages that works?

- Gergely

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.