Email Gateway (Aug 18 2022 at 12:24): Email Gateway (Aug 18 2022 at 12:24):From: merz@loria.fr
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:
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
Email Gateway (Aug 18 2022 at 12:24):From: Makarius <makarius@sketis.net>
On Tue, 16 Sep 2008, merz@loria.fr wrote:
- 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
I have only tried XP/SP3 myself (where everything works), but Vista might
be the problem.
mkdir: cannot create directory `/tmp/isabelle-user\r5992': No such file or
directory
Since there is a strange CR (\r) showing up here, the problem might also
stem from DOS style CRLF conversion. When installing Cygwin there is a
global option to enable this; the (RECOMMENDED) default is plain
Unix/binary mode whithout implicit conversion.
In general Isabelle expects proper Posix semantics for all basic system
operations. Cygwin is surprisingly good at this, turning alien windows
into a solid Posix environment (sometimes even better than Mac OS).
Makarius
Email Gateway (Aug 18 2022 at 12:25):From: Dirk Leinenbach <Dirk.Leinenbach@dfki.de>
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
Hi,
I'm using XP/SP3 and I'm sometimes also noticing core dumps from time to
time when using Isabelle2008 with polyml 5.2 (not very frequently
however). Most of these crashes happen directly after starting Isabelle.
A second run with the same theories works fine most of the time. When I
manage to get Isabelle running without core dump it usually runs fine
for the rest of the session even when I work with large theory bodies.
I'm also using Isabelle2005 with (the CVS version of) polyml 5.2. This
was a little bit tricky to install (I had to apply some patches to
Isabelle's ml code) but thanks to Makarius it runs fine now.
Unfortunately, I don't have an error message of the Isabelle2008 core
dumps anymore, but as soon as it happens again, I will send it to the list.
Best regards,
Dirk
Dirk Leinenbach
German Research Center for Artificial Intelligence
Saarbrücken, Germany
Building E1 1, Room 4.06
phone: +49 - 681 / 302 - 57379
fax: +49 - 681 / 302 - 4132
Deutsches Forschungszentrum fuer Kuenstliche Intelligenz GmbH Trippstadter
Strasse 122, D-67663 Kaiserslautern, Germany
Geschaeftsfuehrung:
Prof. Dr. Dr. h.c. mult. Wolfgang Wahlster (Vorsitzender)
Dr. Walter Olthoff
Vorsitzender des Aufsichtsrats:
Prof. Dr. h.c. Hans A. Aukes
Amtsgericht Kaiserslautern, HRB 2313
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.8 (MingW32)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org
iEYEARECAAYFAkjQCXIACgkQvSh4MWGcON8UCgCfeYFMmhdjnIIIVwj/Z6E0l2mO
ZaEAnipaCqmd5hzN5Qo9UxR1z2YUBMbB
=1K3Z
-----END PGP SIGNATURE-----
Last updated: May 03 2024 at 08:18 UTC