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
> 
> ========Messsage================
> command-line-1: Cannot open load file: /cygdrive/c/Win16App/isabelle/ProofGeneral/isar/interface-setup.el
> ========Message=================
> 
> 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


	Makarius





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