Email Gateway (Aug 18 2022 at 12:49): Email Gateway (Aug 18 2022 at 12:49):From: Makarius <makarius@sketis.net>
MKS is the problem. You really need Cygwin here, with full bash and perl,
and regular Posix semantics of everything.
Also make sure that packages "xinit" and "xterm" of Cygwin are installed
-- the Cygwin/X people have changed a few things recently.
Makarius
Email Gateway (Aug 18 2022 at 12:50):From: manish surolia <mani_surolia@yahoo.com>
Hi,
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?
Thanks in advance
Best Regards
Manish Surolia
Add more friends to your messenger and enjoy! Go to http://messenger.yahoo.com/invite/
Email Gateway (Aug 18 2022 at 12:50):From: Makarius <makarius@sketis.net>
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
Last updated: May 03 2024 at 04:19 UTC