Re: [isabelle] Problems in isabelle installation
On Mon, 12 Jan 2009, manish surolia wrote:
> Thanks for the reply.
> I have downloaded the Cygwin and installed it in my PC.
> and Isabelle is installed as below:
> D:\DOCS\isabelle_setup_windows>tar -C C:\Win16App\isabelle\ -xzf Isabelle2008.tar.gz
> D:\DOCS\isabelle_setup_windows>tar -C C:\Win16App\isabelle\ -xzf ProofGeneral.tar.gz
> D:\DOCS\isabelle_setup_windows>tar -C C:\Win16App\isabelle\ -xzf polyml_x86-cygwin.tar.gz
> D:\DOCS\isabelle_setup_windows>tar -C C:\Win16App\isabelle\ -xzf HOL_x86-cygwin.tar.gz
> now I am facing some other problem.
> emacs shows the below message when I run the commond:
> C:\Win16App\isabelle\Isabelle2008\bin>sh Isabelle
> command-line-1: Cannot open load file: /cygdrive/c/Win16App/isabelle/ProofGeneral/isar/interface-setup.el
> Could you please help me to solve this issue also?
Is the above tar invocation from MKS or Cygwin? Since the paths are given
in windows notation, I would guess it is probably not Cygwin, and
unpacking the tar did not fully observe the Posix file system view.
This might well be relevant here, because of symbolic links contained in
the archives. In particular, isabelle/ProofGeneral should be a link
pointing to something isabelle/ProofGeneral-3.7.1, but it may have got
garbled in the windows file system. (If everything is done via Cygwin,
symblinks come out correctly for any other Cygwin tools.)
Moreover, to get XEmacs running in the end, start your X11 session within
Cygwin like this:
startx /usr/bin/xterm -- -multiwindow
And then the Isabelle Proof General interface like this:
isabelle-interface -p xemacs -x true
This archive was generated by a fusion of
Pipermail (Mailman edition) and