Email Gateway (Aug 17 2022 at 13:46): Email Gateway (Aug 17 2022 at 13:46):From: Martin Ellis <m.a.ellis@ncl.ac.uk>
On Wednesday 15 February 2006 06:04, Jean-Francois Molderez wrote:
I have tried to install Xemacs and Isabelle but there is still ( after
numerous trials) a problem:
When I submit a theory , I get the following :Unknown logic "HOL" -- no heap file found in:
/home/jean-francois/isabelle/heaps/polyml_x86-linux
/home/jean-francois/Programs/Isabelle/Isabelle2005/heaps/polyml_x86-linux
Have you tried running the ./build script from
Programs/Isabelle/Isabelle2005 ?
There are also these warning about the mule-packages ( what is mule ???)
that I receive when starting Isabelle /Xemacs :
Mule provides support for displaying non-European characters in XEmacs.
According to the ProofGeneral FAQ, you need it.
I don't know about others, but Debian-based linux distributions provide
separate XEmacs packages that have mule support. If your distribution
doesn't have these packages, you might need to recompile XEmacs.
Martin
Email Gateway (Aug 17 2022 at 13:46):From: Jean-Francois Molderez <jfmolderez@hotmail.com>
I have tried to install Xemacs and Isabelle but there is still ( after
numerous trials) a problem:
When I submit a theory , I get the following :
Unknown logic "HOL" -- no heap file found in:
/home/jean-francois/isabelle/heaps/polyml_x86-linux
/home/jean-francois/Programs/Isabelle/Isabelle2005/heaps/polyml_x86-linux
There are also these warning about the mule-packages ( what is mule ???)
that I receive when starting Isabelle /Xemacs :
(1) (warning/warning) Autoload error in:
//usr/share/xemacs/mule-packages/lisp/skk/auto-autoloads:
Cannot open load file: mule
(2) (warning/warning) Autoload error in:
//usr/share/xemacs/mule-packages/lisp/lookup/auto-autoloads:
Cannot open load file: mule
(3) (warning/warning) Autoload error in:
//usr/share/xemacs/mule-packages/lisp/latin-euro-standards/auto-autoloads:
Symbol's function definition is void: find-charset
Thank you for any help.
Jean-Franois Molderez
Free blogging with MSN Spaces http://spaces.msn.com/?mkt=nl-be
Email Gateway (Aug 17 2022 at 13:46):From: nipkow@in.tum.de
There are also these warning about the mule-packages ( what is mule ???)
that I receive when starting Isabelle /Xemacs :
There are two versions of xemacs, with and without mule (MUlti-Lingual
Emacs). When you install xemacs, you need to beware of this. Hence our
installation hint "with mule support". Without mule, you can get very strange
effects in ProofGeneral.
Tobias
Email Gateway (Aug 17 2022 at 13:46):From: Alexander Krauss <krauss@in.tum.de>
nipkow@in.tum.de wrote:
Also, your first error message means that the HOL image (i.e. the
precompiled image with the HOL logic and all pre-proved theorems) is
missing. Assuming that you are installing the Isabelle2005 release, make
sure that you have downloaded and installes the image, which is a
seperate download under "Precompiled logics". In fact, make sure that
you exactly follow the installation instructions on the webpage,
especially if it is the first time you install Isabelle.
If this doesn't help, please ask again with more information (your
architecture/OS, which Isabelle version, which xemacs, what you did...)
Alex
Last updated: May 03 2024 at 12:27 UTC