Email Gateway (Aug 18 2022 at 14:23): Email Gateway (Aug 18 2022 at 14:23):From: "Li, Chanjuan" <lichanjuan04@gmail.com>
hi,all:
I am newbie of isabelle. When I use proof general, I can not fulfil
proof successfully. Software of my machine is as follows:
*)Linux OS
*) Isabelle2009
*) polyml-5.2.1 (for x86, but my machine is x86_64)
*) proofgeneral-3.7.1
*) xemacs 21.7
I follow the proof general user manual, the proof process always in
queue region( appear pink) and stalled. I can not undo. I look at the
shell buffer, the proof script can not feed into proof shell. I have no
idea what happened, can anyone help me? thanks in advance.
lily
Email Gateway (Aug 18 2022 at 14:23):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Lily,
ProofGeneral is indeed a challenge to get run. Most care is required
choosing an appropriate emacs version. Concerning the XEmacs series,
XEmacs 21.7 is not expected to work. XEmacs 21.4.* should work as a
last resort. Definitely preferable is GNU Emacs 22 (or 23). See
further http://isabelle.in.tum.de/installation.html. Note that recently
a new Isabelle2009-1 has been released (together with a suitable polyml
and pg), which you should use anyway unless you have strong reasons to
stick with Isabelle2009.
Hope this helps
Florian
signature.asc
Last updated: Apr 25 2024 at 16:19 UTC