Email Gateway (Aug 18 2022 at 13:49): Email Gateway (Aug 18 2022 at 13:49):From: Randy Pollack <rpollack@inf.ed.ac.uk>
Hi,
My computer support group just moved my home directory from NFS to AFS
(distributed file system).
I'm having trouble running isabelle with xsymbols. (GNU Emacs 22.3.1)
isabelle emacs -p emacs mythy.thy
In the emacs Warnings buffer I see
Error (x-symbol): Couldn't add /afs/inf.ed.ac.uk/user/r/rpollack/work/tools/isabelle2009/ProofGeneral/x-symbol/etc/pcf/ to X font path
Warning (emacs): X-Symbol characters with registry "iso8859-3" are not used
Warning (emacs): X-Symbol characters with registry "iso8859-9" are not used
Warning (emacs): X-Symbol characters with registry "iso8859-15" are not used
Warning (emacs): X-Symbol characters with registry "xsymb-xsymb1" are not used
Symbols are not displayed in the .thy buffer: \<forall>, \<And>, etc.
/afs/inf.ed.ac.uk/user/r/rpollack/work/tools/isabelle2009/ProofGeneral/x-symbol/etc/pcf/
exists, and has expected permissions
Thanks for any help.
Randy
Email Gateway (Aug 18 2022 at 13:49):From: Makarius <makarius@sketis.net>
Strange. Maybe Emacs just does not like AFS.
You can try to use these fonts via the X11 fontserver protocol, e.g. like
this in your Isabelle settings file:
XSYMBOL_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"
This refers to a public font service at TUM.
Makarius
Email Gateway (Aug 18 2022 at 13:50):From: Randy Pollack <rpollack@inf.ed.ac.uk>
Hi,
Lucas Dixon figured this out.
Apparently the x-server runs as a process owned by root(?) but not by
me, so my AFS authorisation doesn't let it read these files.
Makarius' suggestion works:
xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200
but obviously is not really satisfactory.
Lucas suggested to make the ProofGeneral/x-symbol/etc/pcf/ directory
readable by system:anyuser
fs setacl -dir SOME_PATH -acl system:anyuser read
This allows ProofGeneral with x-symbols to apparently work (I don't see
any problem) although, mysteriously, on startup of ProofGeneral I
still get the error message
Error (x-symbol): Couldn't add
/afs/inf.ed.ac.uk/user/r/rpollack/work/tools/isabelle2009/ProofGeneral/x-symbol/etc/pcf/
to X font path
in my Warnings buffer.
Randy
--
Makarius writes:
On Wed, 15 Jul 2009, Randy Pollack wrote:
My computer support group just moved my home directory from NFS to AFS
(distributed file system).I'm having trouble running isabelle with xsymbols. (GNU Emacs 22.3.1)
isabelle emacs -p emacs mythy.thy
In the emacs Warnings buffer I see
Error (x-symbol): Couldn't add /afs/inf.ed.ac.uk/user/r/rpollack/work/tools/isabelle2009/ProofGeneral/x-symbol/etc/pcf/ to X font path
/afs/inf.ed.ac.uk/user/r/rpollack/work/tools/isabelle2009/ProofGeneral/x-symbol/etc/pcf/
exists, and has expected permissionsStrange. Maybe Emacs just does not like AFS.
You can try to use these fonts via the X11 fontserver protocol, e.g. like
this in your Isabelle settings file:XSYMBOL_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"
This refers to a public font service at TUM.
Makarius
--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
Email Gateway (Aug 18 2022 at 13:50):From: Randy Pollack <rpollack@inf.ed.ac.uk>
Sorry, my last email was wrong. Because X is stateful I didn't
understand the situation.
Lucas suggested to make the ProofGeneral/x-symbol/etc/pcf/ directory
readable by system:anyuser
In order to do this, you must make the entire path, from your home
directory down to the pcf directory readable to system:anyuser, which
is not a real solution.
For the moment, I copied the pcf directory to a non-AFS filesystem.
Randy
Email Gateway (Aug 18 2022 at 15:36):From: Makarius <makarius@sketis.net>
On Thu, 1 Jul 2010, 许庆国 wrote:
When I start Isabelle2009-2 In XEmacs 21.4 under cygwin 1.7 , the following warning and error messages show.
(1) (x-symbol/error) Couldn't add /usr/local/Isabelle2009-2/contrib/ProofGeneral/x-symbol/etc/pcf/ to X font path
(2) (x-symbol/error) Couldn't add /usr/local/Isabelle2009-2/contrib/ProofGeneral/x-symbol/etc/pcf/ to X font pathBut the Isabelle 2009-1 works fine.
In principle there should be no difference of Isabelle2009-1 vs.
Isabelle2009-2 here -- at least in the standard distribution bundles,
which contain exactly the same version of ProofGeneral-3.7.1.1.
According to the following mail, I have tried sereval methods:
1) xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200
gives the following errors message:
================================================
xset: bad font path element (#23), possible causes are:
Directory does not exist or has wrong permissions
Directory missing fonts.dir
Incorrect font server address or syntax
================================================
This used to work until a few months ago -- either our font service is
broken, or there have been some protocol changes in X.org that the server
does not understand. Since X-Symbol and X11 fonts are being phased out
eventually, it is not worth investing too much time on it.
================================================
2 [main] xemacs-21.4.22 2960 exception::handle: Exception: STATUS_ACCESS_VIOLATION
805 [main] xemacs-21.4.22 2960 open_stackdumpfile: Dumping stack trace to xemacs-21.4.22.exe.stackdump
2 [main] xemacs-21.4.22 200 exception::handle: Exception: STATUS_ACCESS_VIOLATION
636 [main] xemacs-21.4.22 200 open_stackdumpfile: Dumping stack trace to xemacs-21.4.22.exe.stackdump
2 [main] xemacs-21.4.22 3852 exception::handle: Exception: STATUS_ACCESS_VIOLATION
643 [main] xemacs-21.4.22 3852 open_stackdumpfile: Dumping stack trace to xemacs-21.4.22.exe.stackdump
2 [main] xemacs-21.4.22 788 exception::handle: Exception: STATUS_ACCESS_VIOLATION
================================================
I've also seen such generic xemacs crashes on cygwin Cccasionally. My
guess is that this is due to the general situation of xemacs being old and
unmaintained for a couple of years.
The reason why ancient xemacs is needed on Cygwin is the lack of GNU Emacs
22 on that platform. ProofGeneral-3.7.x does not work with the newer GNU
Emacs 23 line, which is generally far superior.
Anyway, the Proof General 4.x code base has again become quite usable, so
you can also try the CVS version from
http://proofgeneral.inf.ed.ac.uk/devel together with GNU Emacs 23 on
Cygwin.
Since there is no X-Symbol mode in that version, you can't get any
problems with it :-) You will need a good Unicode font with math symbols,
though. Isabelle2009-2/lib/fonts/IsabelleText.ttf can be installed
manually on Windows and then configured as default font inside Emacs.
That's not perfect, but much better than anything we've ever had so far.
Maybe David Aspinall can provide a proper development snapshot of the
current Proof General CVS.
Makarius
Email Gateway (Aug 18 2022 at 15:37):From: Timothy McKenzie <tjm1983@gmail.com>
I use Proof General 3.7.1.1 with GNU Emacs 23.2.1, but I'm working
with Linux (and NetBSD on another computer, with perhaps a
different release of Emacs 23), not Cygwin. I find it usable
(with Unicode tokens, not X-Symbol), but not perfect. For
details, see my post at http://tinyurl.com/22m7mbq and David
Aspinall's commendably concise summary in his reply.
Tim
<><
signature.asc
Email Gateway (Aug 18 2022 at 15:38):From: Makarius <makarius@sketis.net>
BTW http://proofgeneral.inf.ed.ac.uk/devel now has an update on the PG
pre-4.0 branch (ProofGeneral-4.0pre100709) that works much better than
earlier versions. That should allow you to use Emacs 23.x without the
traps and pitfalls of old PG 3.7.x on that platform.
Any issues should be directed to http://proofgeneral.inf.ed.ac.uk/trac/
Makarius
Email Gateway (Aug 18 2022 at 15:40):From: 许庆国 <qgxu@mail.shu.edu.cn>
Hi:
I have also encountered the same problem.
When I start Isabelle2009-2 In XEmacs 21.4 under cygwin 1.7 , the following warning and error messages show.
(1) (x-symbol/error) Couldn't add /usr/local/Isabelle2009-2/contrib/ProofGeneral/x-symbol/etc/pcf/ to X font path
(2) (x-symbol/error) Couldn't add /usr/local/Isabelle2009-2/contrib/ProofGeneral/x-symbol/etc/pcf/ to X font path
(3) (x-symbol/warning) Cannot find font in -adobe-helvetica_sub-medium-r-normal--12------iso8859-1
(4) (x-symbol/warning) Cannot find font in -adobe-helvetica_sup-medium-r-normal--12------iso8859-1
(5) (x-symbol/warning) Cannot find font in -adobe-helvetica_sub-medium-r-normal--12------iso8859-2, -etl-fixed_sub-medium-r-normal--14-140-72-72-c-*-iso8859-2
(6) (x-symbol/warning) Cannot find font in -adobe-helvetica_sup-medium-r-normal--12------iso8859-2, -etl-fixed_sup-medium-r-normal--14-140-72-72-c-*-iso8859-2
(7) (x-symbol/warning) Cannot find font in -adobe-helvetica_sub-medium-r-normal--12------iso8859-3, -etl-fixed_sub-medium-r-normal--14-140-72-72-c-*-iso8859-3
(8) (x-symbol/warning) Cannot find font in -adobe-helvetica_sup-medium-r-normal--12------iso8859-3, -etl-fixed_sup-medium-r-normal--14-140-72-72-c-*-iso8859-3
(9) (warning/warning) X-Symbol characters with registry "iso8859-9" are not used
(10) (warning/warning) X-Symbol characters with registry "iso8859-15" are not used
(11) (x-symbol/warning) Cannot find font in -xsymb-xsymb0_sub-medium-r-normal--12--75-75-p--adobe-fontspecific, -adobe-symbol_sub-medium-r-normal---120-----adobe-fontspecific
(12) (x-symbol/warning) Cannot find font in -xsymb-xsymb0_sup-medium-r-normal--12--75-75-p--adobe-fontspecific, -adobe-symbol_sup-medium-r-normal---120-----adobe-fontspecific
(13) (warning/warning) X-Symbol characters with registry "xsymb-xsymb1" are not used
But the Isabelle 2009-1 works fine.
According to the following mail, I have tried sereval methods:
1) xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200
gives the following errors message:
================================================
xset: bad font path element (#23), possible causes are:
Directory does not exist or has wrong permissions
Directory missing fonts.dir
Incorrect font server address or syntax
================================================
2) fs setacl -dir SOME_PATH -acl system:anyuser read
"fs" is not accessed in my cygwin.
3) I don't understand the "copied the pcf directory to a non-AFS filesystem".
I copied pcf to "C:\cygwin\usr" and then start Isabelle through the command
/usr/local/Isabelle/bin/isabelle emacs -p xemacs
the following messages answer me.
================================================
2 [main] xemacs-21.4.22 2960 exception::handle: Exception: STATUS_ACCESS_VIOLATION
805 [main] xemacs-21.4.22 2960 open_stackdumpfile: Dumping stack trace to xemacs-21.4.22.exe.stackdump
2 [main] xemacs-21.4.22 200 exception::handle: Exception: STATUS_ACCESS_VIOLATION
636 [main] xemacs-21.4.22 200 open_stackdumpfile: Dumping stack trace to xemacs-21.4.22.exe.stackdump
2 [main] xemacs-21.4.22 3852 exception::handle: Exception: STATUS_ACCESS_VIOLATION
643 [main] xemacs-21.4.22 3852 open_stackdumpfile: Dumping stack trace to xemacs-21.4.22.exe.stackdump
2 [main] xemacs-21.4.22 788 exception::handle: Exception: STATUS_ACCESS_VIOLATION
================================================
but the apperance of PG's X symbol looks well this time.
what's the reason about these things.
thank you very much in advance!
2010-07-01
许庆国
Last updated: Apr 26 2024 at 08:19 UTC