Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] InstallProblem with Proofgeneral

view this post on Zulip Email Gateway (Aug 18 2022 at 12:46):

From: Peter Ulrich <Peter.Ulrich1975@gmx.de>
Hi,

I have installed xemacs 21.4.21 installed.
I have downloaded and installed the files from the Isabelle website.
When running
/usr/local/Isabelle/bin/Isabelle -p xemacs

xemacs opens together with PG;
when I try to make a step (e.g., next) I get the error:
"Symbol's value as variable is void: proof-toolbar-next"

when trying to enable x-symbol, I get the message:
"Symbol's function definition is void: quail-define-package"
when disabling x-symbol and enabling it again I get:
"Wrong type argument: arrayp, nil"

view this post on Zulip Email Gateway (Aug 18 2022 at 12:47):

From: Makarius <makarius@sketis.net>
This looks like the usual Emacs compatibility problems of Proof General.
Even though XEmacs is still advertized as default for Isabelle2008, GNU
Emacs 22 works usually better.

Makarius

Last updated: May 03 2024 at 04:19 UTC