[isabelle] Isabelle Installation



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/





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.