Email Gateway (Aug 18 2022 at 10:47): Email Gateway (Aug 18 2022 at 10:47):From: JanuGerman <doublemalam@yahoo.co.uk>
Hi Every one,
I am stuck in Isabelle installation. I was using Isabelle from IsoMorph, from quite time, but its too slow.
I tried Installing Isabelle many times, but always, got this error.
Can any body help in sorting out this.
Regards,
The error is as follows:
(1) (file-mode-spec/warning) Error in File mode specification: Cannot open load file: "executable"
Backtrace follows:
signal(file-error ("Cannot open load file" "executable"))
# bind (path handler filename nosuffix nomessage noerror file)
load("executable" nil nil nil)
# (unwind-protect ...)
executable-find("isabelle")
# bind (exec-path extrapath returnnopath progname)
proof-locate-executable("isabelle" t ("/usr/local/Isabelle/bin/" "/opt/Isabelle/bin/" "/usr/Isabelle/bin/" "/usr/share/Isabelle/bin/"))
(if (fboundp (quote proof-running-on-win32)) "C:\\sml\\bin\\.run\\run.x86-win32.exe @SMLload=C:\\Isabelle\\" (proof-locate-executable "isabelle" t (quote ("/usr/local/Isabelle/bin/" "/opt/Isabelle/bin/" "/usr/Isabelle/bin/" "/usr/share/Isabelle/bin/"))))
eval((if (fboundp (quote proof-running-on-win32)) "C:\\sml\\bin\\.run\\run.x86-win32.exe @SMLload=C:\\Isabelle\\" (proof-locate-executable "isabelle" t (quote ("/usr/local/Isabelle/bin/" "/opt/Isabelle/bin/" "/usr/Isabelle/bin/" "/usr/share/Isabelle/bin/")))))
# bind (value symbol)
custom-initialize-reset(isabelle-program-name (if (fboundp (quote proof-running-on-win32)) "C:\\sml\\bin\\.run\\run.x86-win32.exe @SMLload=C:\\Isabelle\\" (proof-locate-executable "isabelle" t (quote ("/usr/local/Isabelle/bin/" "/opt/Isabelle/bin/" "/usr/Isabelle/bin/" "/usr/share/Isabelle/bin/")))))
# bind (initialize requests args doc default symbol)
custom-declare-variable(isabelle-program-name (if (fboundp (quote proof-running-on-win32)) "C:\\sml\\bin\\.run\\run.x86-win32.exe @SMLload=C:\\Isabelle\\" (proof-locate-executable "isabelle" t (quote ("/usr/local/Isabelle/bin/" "/opt/Isabelle/bin/" "/usr/Isabelle/bin/" "/usr/share/Isabelle/bin/")))) "*Default name of program to run Isabelle.\n\nThe default value except when running under Windows is \"isabelle\",\nwhich will get expanded using PATH if possible, or in a number\nof standard locations (/usr/local/Isabelle/, /opt/Isabelle, etc). \n\nThe default value when running under Windows is:\n\n C:\\sml\\bin\\.run\\run.x86-win32.exe @SMLload=C:\\Isabelle\\\n\nThis expects SML/NJ in C:\\sml and Isabelle images in C:Isabelle. \nThe logic image name is tagged onto the end. \n\nNB: The Isabelle settings mechanism or the environment variable\nISABELLE will always override this setting." :type file :group isabelle)
# (unwind-protect ...)
# (unwind-protect ...)
# (unwind-protect ...)
# (unwind-protect ...)
# (unwind-protect ...)
# (unwind-protect ...)
# (unwind-protect ...)
# (unwind-protect ...)
load-internal("isabelle-system" nil require nil binary)
# bind (path handler filename nosuffix nomessage noerror file)
load("isabelle-system" nil require nil)
# (unwind-protect ...)
require(isabelle-system)
byte-code("..." [proof-home-directory load-path require proof "isa/" isabelle-system] 2)
# (unwind-protect ...)
# (unwind-protect ...)
# (unwind-protect ...)
# (unwind-protect ...)
# (unwind-protect ...)
# (unwind-protect ...)
# (unwind-protect ...)
# (unwind-protect ...)
load-internal("isar" nil nil nil binary)
# bind (path handler filename nosuffix nomessage noerror file)
load("isar")
# bind (library)
load-library("isar")
(cond ((and (boundp (quote proof-assistant)) (not (string-equal proof-assistant ""))) (or (string-equal proof-assistant "Isabelle") (message (concat "Isabelle" " Proof General error: Proof General already in use for " proof-assistant)))) (t (proof-ready-for-assistant "Isabelle" (quote isar)) (load-library "isar") (isar-mode)))
isar-mode()
# bind (alist mode name keep-going)
# (unwind-protect ...)
# bind (just-from-file-name)
set-auto-mode()
#<compiled-function nil "...(5)" [set-auto-mode t] 1>()
# (unwind-protect ...)
call-with-condition-handler(#<compiled-function (__call_trapping_errors_arg__) "...(17)" [__call_trapping_errors_arg__ errstr error-message-string lwarn file-mode-spec warning "Error in %s: %s\n\nBacktrace follows:\n\n%s" "File mode specification" backtrace-in-condition-handler-eliminating-handler] 8> #<compiled-function nil "...(5)" [set-auto-mode t] 1>)
# (condition-case ... . ((error)))
# bind (find-file)
normal-mode(t)
# bind (nomodes after-find-file-from-revert-buffer noauto warn error)
after-find-file(t t)
# (unwind-protect ...)
# bind (inhibit-read-only error number truename rawfile nowarn filename buf)
find-file-noselect-1(#<buffer "Scratch.thy"> "/root/Scratch.thy" nil nil "/root/Scratch.thy" nil)
byte-code("..." [number truename rawfile nowarn filename buf set-buffer-major-mode find-file-noselect-1] 7)
# (condition-case ... . ((t (byte-code "Â!Ã @ A\"" [buf data kill-buffer signal] 3))))
# bind (number truename buf wildcards rawfile nowarn filename)
find-file-noselect("/root/Scratch.thy" nil nil nil)
# bind (wildcards codesys filename)
find-file("/root/Scratch.thy")
# bind (dir file-count line end-of-options file-p arg tem)
command-line-1()
# bind (command-line-args-left)
command-line()
# (condition-case ... . ((t (byte-code " Â" [error-data data nil] 1))))
# bind (error-data)
normal-top-level()
# (condition-case ... . error)
# (catch top-level ...)
___________________________________________________________
Yahoo! Answers - Got a question? Someone out there knows the answer. Try it
now.
http://uk.answers.yahoo.com/
Email Gateway (Aug 18 2022 at 10:47):From: Makarius <makarius@sketis.net>
On Fri, 31 Aug 2007, JanuGerman wrote:
I am stuck in Isabelle installation. I was using Isabelle from IsoMorph,
from quite time, but its too slow.
IIRC IsaMorph uses SML/NJ, which is a bit sluggish. We get best results
with Poly/ML, either the patched version version 4.1.4 (see
http://isabelle.in.tum.de/installation.html) or more recent 5.0 (see
http://www4.in.tum.de/~wenzelm/test/Isabelle2005-polyml-5.0.tar.gz).
I tried Installing Isabelle many times, but always, got this error.
The error is as follows: (1) (file-mode-spec/warning) Error in File mode
specification: Cannot open load file: "executable"
This is just one of the usual problems of getting Proof General work with
a certain version of Emacs. See
http://isabelle.in.tum.de/installation.html for some further hints. In
particular, you should first try to get the basic isabelle-process
running.
Makarius
Email Gateway (Aug 18 2022 at 10:48):From: JanuGerman <doublemalam@yahoo.co.uk>
Thanks for your response.
Unfortunately, still i am not able to run Isabelle.
As you suggested to run the basic Isabelle process, so that is done by using the following command
/usr/local/Isabelle/bin/isabelle-process -I
This command works perfectly, and it means the Isabelle process is running perfectly.
I tried to get the latest version but still the same problem.
I think so, it is a compatibilty problem with XEmacs, Would you kindly suggest me a compatible version, of XEMACS, or some installation steps in this regard.
Regards,
----- Original Message ----
From: Makarius <makarius@sketis.net>
To: JanuGerman <doublemalam@yahoo.co.uk>
Cc: isabelle-users@cl.cam.ac.uk
Sent: Friday, 31 August, 2007 9:45:46 AM
Subject: Re: [isabelle] Isabelle Installation
On Fri, 31 Aug 2007, JanuGerman wrote:
I am stuck in Isabelle installation. I was using Isabelle from IsoMorph,
from quite time, but its too slow.
IIRC IsaMorph uses SML/NJ, which is a bit sluggish. We get best results
with Poly/ML, either the patched version version 4.1.4 (see
http://isabelle.in.tum.de/installation.html) or more recent 5.0 (see
http://www4.in.tum.de/~wenzelm/test/Isabelle2005-polyml-5.0.tar.gz).
I tried Installing Isabelle many times, but always, got this error.
The error is as follows: (1) (file-mode-spec/warning) Error in File mode
specification: Cannot open load file: "executable"
This is just one of the usual problems of getting Proof General work with
a certain version of Emacs. See
http://isabelle.in.tum.de/installation.html for some further hints. In
particular, you should first try to get the basic isabelle-process
running.
Makarius
___________________________________________________________
Want ideas for reducing your carbon footprint? Visit Yahoo! For Good http://uk.promotions.yahoo.com/forgood/environment.html
Email Gateway (Aug 18 2022 at 10:48):From: Makarius <makarius@sketis.net>
This depends on your OS platform. Usually a self-compile of the stable
branch of xemacs works (using mule and sumo).
You may also try GNU emacs, by telling Isabelle about it via option -p of
the interface script, or setting PROOF_GENERAL_OPTIONS in etc/settings.
Makarius
Last updated: May 03 2024 at 08:18 UTC