Email Gateway (Aug 18 2022 at 11:28): Email Gateway (Aug 18 2022 at 11:28):From: Mitchell Wand <wand@ccs.neu.edu>
Hi,
I'm trying to run the cygwin version of isabelle from my Windows Gnu Emacs
22.1. I successfully built isabelle from the cygwin-x86 image, calling
"build" to compile HOL. When I call "isabelle" from a cygwin bash window, I
get
val it = () : unit
val commit = fn : unit -> bool
ML>
which I'm assuming is right.
I have set isabelle-program-name to point to a batch file that sits in the
emacs bin directory. The latest version of the batch file says:
rem @echo off
rem set ISATOP=/usr/local/Isabelle2007
rem set ISALIB=%ISATOP%/lib
set ISABINWINDOWS=C:\Cygwin\usr\local\Isabelle2007\bin
rem set ISABIN=%ISATOP%/bin
rem set PATH=%PATH%;%ISABIN%
rem set HOME=%HOMEPATH%
bash %ISABINWINDOWS%\isabelle-process %1 %2 %3
(This is based on a working script to call coq from proof general).
When I do this, I get the following in the response buffer:
*** Exception-
*** ERROR "Illegal character(s) \":\" in path element specification:
\"c:\""
*** raised
*** At command "ML_command".
It looks like I'm actually reaching some part of the isabelle system, but
something is finding a Windows path when it's looking for a cygwin path.
Anybody have any guesses as to what this might be?
--Mitch Wand
PS: Yes, I've tried running isabelle-interface-- this pops up a Gnu Emacs
under X and starts Proof General, but I get File mode specification error:
(file-error "Searching for program" "no such file or directory"
"C:\\cygwin\\bin\\tcsh.exe") . Since I use my native Windows emacs for
everything else, I'd like to pursue that line first.
Email Gateway (Aug 18 2022 at 11:28):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear Mitchell,
rem @echo off
rem set ISATOP=/usr/local/Isabelle2007
rem set ISALIB=%ISATOP%/lib
set ISABINWINDOWS=C:\Cygwin\usr\local\Isabelle2007\bin
rem set ISABIN=%ISATOP%/bin
rem set PATH=%PATH%;%ISABIN%
rem set HOME=%HOMEPATH%
bash %ISABINWINDOWS%\isabelle-process %1 %2 %3
one possible solution: use cygwin path convention for ISABINWINDWOS,
e.g. /cygdrive/c/Cyhwin/usr/local/Isabelle2007/bin
PS: Yes, I've tried running isabelle-interface-- this pops up a Gnu Emacs
under X and starts Proof General, but I get File mode specification error:
(file-error "Searching for program" "no such file or directory"
"C:\\cygwin\\bin\\tcsh.exe") . Since I use my native Windows emacs for
everything else, I'd like to pursue that line first.
This indeed sounds very strange since Isabelle only relies on bash, not
tcsh. Have you tried Cygwin/XEmacs? E.g by "isabelle-interface -p
xemacs"? Cygwin/XEmacs is known to work with Isabelle/PG reasonably
whereas there are no experience reports for Cygwin/GNUEmacs
Hope this helps
Florian
signature.asc
Email Gateway (Aug 18 2022 at 11:28):From: Makarius <makarius@sketis.net>
Last time I've checked our packages from the Isabelle download area did
work on Cygwin out of the box, either with GNU Emacs 21.x and XEmacs 21.x.
You should make sure that Proof General is the one from our site! I did
not try GNU Emacs 22 on Cygwin, but it works on Ubuntu Linux.
Your attempt at using a windows version of Emacs is very unlikely to
succeed. I've never seen it work, and what I known from the internals of
the whole arrangement it would require a lot of extra efforts (there are
very few native windows users out there).
Makarius
Email Gateway (Aug 18 2022 at 11:29):From: Mitchell Wand <wand@ccs.neu.edu>
On Thu, Feb 28, 2008 at 3:49 AM, Florian Haftmann <
florian.haftmann@informatik.tu-muenchen.de> wrote:
PS: Yes, I've tried running isabelle-interface-- this pops up a Gnu
Emacs
under X and starts Proof General, but I get File mode specification
error:
(file-error "Searching for program" "no such file or directory"
"C:\\cygwin\\bin\\tcsh.exe") . Since I use my native Windows emacs for
everything else, I'd like to pursue that line first.This indeed sounds very strange since Isabelle only relies on bash, not
tcsh. Have you tried Cygwin/XEmacs? E.g by "isabelle-interface -p
xemacs"? Cygwin/XEmacs is known to work with Isabelle/PG reasonably
whereas there are no experience reports for Cygwin/GNUEmacs
And Markarius said:
Last time I've checked our packages from the Isabelle download area did
work on Cygwin out of the box, either with GNU Emacs 21.x and XEmacs 21.x.
You should make sure that Proof General is the one from our site! I did
not try GNU Emacs 22 on Cygwin, but it works on Ubuntu Linux.
OK, you guys have convinced me to try running emacs from cygwin. -- I can't
imagine how I'd get the X-symbol stuff to work via windows.
Interestingly, putting (setq debug-on-error t) didn't seem to work, but I
eventually figured out that the reference to tcsh.exe was coming from my
Windows SHELL variable. Changing that to /usr/bin/bash worked like a
charm. I now have what appears to be a working isabelle/GnuEmacs21.2/cygwin
stack.
Now all I have to do is find the time to play with it.
Thanks.
--Mitch
Email Gateway (Aug 18 2022 at 11:29):From: Yasuhiko Minamide <minamide@score.cs.tsukuba.ac.jp>
I'm using the same combination for several years with a personally patched
version of Isabelle. It might also work for you.
The code below just converts a Windows path into a cygwin path by calling
"cygpath" command of cygwin.
Yasuhiko Minamide
diff -cr Isabelle_08-May-2007/src/Pure/General/path.ML Isabelle_08-May-2007-windows/src/Pure/General/path.ML
*** Isabelle_08-May-2007/src/Pure/General/path.ML Fri Dec 15 08:08:09 2006
--- Isabelle_08-May-2007-windows/src/Pure/General/path.ML Wed May 9 10:40:14 2007
* 120,129 **
val explode_elems = map explode_elem o filter_out (fn c => c = "" orelse c = ".");
! fun explode_path str = Path (norm
(case space_explode "/" str of
"" :: ss => Root :: explode_elems ss
! | ss => explode_elems ss));
(* base element *)
--- 120,138 ----
val explode_elems = map explode_elem o filter_out (fn c => c = "" orelse c = ".");
! (* fun explode_path str = Path (norm
(case space_explode "/" str of
"" :: ss => Root :: explode_elems ss
! | ss => explode_elems ss)); *)
!
! fun explode_path str =
! let val str = execute ("cygpath "^str)
! val str = String.substring (str, 0, String.size str - 1) in
! Path (norm
! (case space_explode "/" str of
! "" :: ss => Root :: explode_elems ss
! | ss => explode_elems ss))
! end;
(* base element *)
Last updated: May 03 2024 at 12:27 UTC