[isabelle] Isabelle/cygwin woes



Dear all,

with a colleague of mine we are experiencing some problems when running Isabelle (in batch mode) under cygwin (see transcript below, TLA+ is a homegrown object logic, but is unrelated to the problem). The first issue is the error message related to the creation of the temporary directory; this is probably due to the mix of slashes and backslashes in the path name. The second issue (which may be related to the first one or not) is that Isabelle core dumps quite frequently and unpredictably whereas it runs just fine when precisely the same command is issued later. The same command reliably runs without any problem under Linux or Mac OS X.

Does anyone have similar problems, or -- even better -- a fix?

For what it's worth, here is some data about the environment:
- Vista - Windows Version 6.0 (Build 6001: Service Pack 1)
- CYGWIN_NT-6.0 1.5.25(0.156/4/2) 2008-06-12 19:34
- polyml_x86-cygwin from the Isabelle2008 download page
- Isabelle 2008 release

Thanks in advance,
Stephan

(** Isabelle invocation crashes **)
isabelle -r -e 'use_thy "test2" handle e => OS.Process.exit OS.Process.failure
; OS.Process.exit OS.Process.success : unit;' TLA+
mkdir: cannot create directory `/tmp/isabelle-user\r5992': No such file or directory /usr/local/Isabelle2008/lib/scripts/run-polyml: line 79: 7288 Segmentation fault (core dumped) "$POLY" -q $ML_OPTIONS
rmdir: failed to remove `/tmp/isabelle-user\r5992': No such file or directory

(** invocation of same command that runs just fine **)
isabelle -r -e 'use_thy "test2" handle e => OS.Process.exit OS.Process.failure
; OS.Process.exit OS.Process.success : unit;' TLA+
mkdir: cannot create directory `/tmp/isabelle-user\r7844': No such file or directory
val it = () : unit
val commit = fn : unit -> bool
Loading theory "test2"
[...]
val it = () : unit
rmdir: failed to remove `/tmp/isabelle-user\r7844': No such file or directory







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