[isabelle] Running cygwin isabelle from windows Gnu Emacs
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
> val it = () : unit
val commit = fn : unit -> bool
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
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:
*** ERROR "Illegal character(s) \":\" in path element specification:
*** 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?
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 archive was generated by a fusion of
Pipermail (Mailman edition) and