Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] proof general stalls at queue region!


view this post on Zulip 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

view this post on Zulip 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