Email Gateway (Aug 19 2022 at 08:57): Email Gateway (Aug 19 2022 at 08:57):From: Makarius <makarius@sketis.net>
Error "no error" sounds like one of these old Windows jokes.
Anyway, such basic shell tools crashing normally indicates some confusion
of Cygwin versions (notably cygwin.dll). Isabelle2012 bundles its own
Cygwin, and you need to make sure that it does not execute programs from a
different Cygwin installation. This should normally work, if you use the
Cygwin Terminal from inside Isabelle2012.
Makarius
Email Gateway (Aug 19 2022 at 08:57):From: Makarius <makarius@sketis.net>
Which is your version of Windows?
Could this be another incident of the virus checker deleting some .exe
files that it does not like?
Makarius
Email Gateway (Aug 19 2022 at 08:57):From: Makarius <makarius@sketis.net>
One more attempt to rescue the Windows situation:
* Use "isabelle getenv ISABELLE_HOME_USER" to determine the place of
your local etc/settings file; it should be something like
.isabelle/Isabelle2012/etc/settings within your normal Windows home directory.
* Create that file and add the following line:
unset EXEC_PROCESS
This should bypass the exec_process C wrapper that I've added in the last
moment before the Isabelle2012 release to address some issues with the
traditional perl wrapper that was still used in some of the RC versions.
Makarius
Email Gateway (Aug 19 2022 at 08:57):From: Makarius <makarius@sketis.net>
On Wed, 10 Oct 2012, Alfio Martini wrote:
I did what you suggested and, although this time that error did not
appear, the compilation process now got stuck (I had to kill it).In between, I installed Isabelle2012 in another W7 desktop machine and
the same problem occurs. So it seems it is not only with my laptop.Actually* I would like to get that RC2* version again which was working
great, Can you provide a link to me? I found the link but it seems the
file is not available anymore.
I've purged these intermediate snapshots some weeks ago. "RC" versions
don't have any official status and are not archived, apart from their
changeset ids:
ec5d5402966416bc2656e9d100e287c208555361 Isabelle2012-RC1
1636ff4c6243b653054e3061d312f7859c67429c Isabelle2012-RC2
ed5f56b8f90ae33ffa10b6eadee2f9433bddc5eb Isabelle2012-RC3
Are you sure that you've had RC2? There are hardly any interesting
changes from Isabelle2012-RC2 to official Isabelle2012.
From RC1 to RC2 quite a few things were going on for Windows in
particular. You were one of the few people giving any feedback on the
release candidates, and I turned your experience report into some changes
that might be relevant here. Before the release I was assuming that you
would follow further RC steps, and interpreted no news as good news. So
maybe we should finish that now.
There are two things between Isabelle2012-RC1 and Isabelle2012-RC2 that
look relevant to your observation.
(1) The Windows installer (7zip with some init.bat) does a "rebaseall"
on all executables. This is meant to prevent Cygwin exe crashes as
you have seen, but it might have an adverse effect as well.
To get a version of Isabelle2012 that is not "rebased" automatically
you can use the Cygwin-Terminal of a version you have already
and download and unpack the following:
http://isabelle.in.tum.de/dist/Isabelle2012_bundle_x86-cygwin.tar.gz
It is important to use Cygwin/GNU tar to unpack it into a place
where you will later find it without Cygwin. Then you exit the
auxiliary Cygwin-Terminal and start the newly unpacked
Isabelle2012/Isabelle.exe or its Cygwin-Terminal from there.
(2) Some accident with perl signals and the poly process. It was
motivated by your initial encounter with Isabelle2012-RC1 where the
antivirus had deleted the executable, but the error was quite
implicit. I had "fixed" that in a way that was causing problems in
other cases later, and maybe even your IsaMakefile now.
The following change from the post-Isabelle2012 period could
improve the situation again:
--- a/lib/scripts/run-polyml Wed Jan 19 21:00:16 2011 +0100
+++ b/lib/scripts/run-polyml Fri May 25 17:14:14 2012 +0200
@@ -74,7 +74,7 @@
fi
"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
Which means it is just "kill -TERM" instead of "kill -HUP" in the
feeder script that is wrapped around poly.
Makarius
Email Gateway (Aug 19 2022 at 08:57):From: Makarius <makarius@sketis.net>
On Thu, 11 Oct 2012, Alfio Martini wrote:
Although I will still keep using JEdit/Isabelle in the W7 setup (it is
just me or does the jEdit interface looks much nicer in windows that in
the linux environment?),
The 2D rendering engine of Java is a bit better on Windows by default.
Speaking of Isabelle2012, it is still classic Java 1.6. The situation
might change again for Java 1.7.
when running "isabelle jedit" in Linux i get the following error message
(failed to start Isabelle Process: Return Code 127).In the "Prover Session/Syslog" there was only this message:
Error code 127;
In principle there should be more error text somewhere. 127 alone means
that the executable is somehow broken. You might have 64bit Linux with
the 32bit version of Isabelle2012. You either need to get the native
64bit version, or install the missing 32bit shared libraries for C/C++ on
Linux.
For the next release, there will be just a "Linux" download both for
32/64bit.
Makarius
Email Gateway (Aug 19 2022 at 08:58):From: Holger Blasum <hbl@sysgo.com>
Hello Alfio,
This also happens to me sometimes when I use Isabelle/jedit on my old
T30 thinkpad with just 1 Gig of RAM. Did you assign enough memory to
your virtual machine (1 Gig is boundary area)? Another "quick fix"
(less beautiful) in situations with little memory is to invoke
Isabelle with the proof general interface.
Best,
Email Gateway (Aug 19 2022 at 08:58):From: Makarius <makarius@sketis.net>
Could well be. If poly does not manage to load its initial environment,
the error feedback by the Isabelle process is not very friendly.
Generally, the hardware baseline for Isabelle2012 is 2 GB / 2 cores.
This means a mid-range laptop from 3 years ago or high-end "air" model
from today should work smoothly. The mid-range hardware from today is
already at 6 GB / 4 cores and the high-end at 8 GB / 8 cores -- I've just
checked at FNAC Paris last Saturday.
Netbooks or other tiny portable devices won't work.
Makarius
Last updated: Apr 25 2024 at 04:18 UTC