Re: [isabelle] (Unexpected) Problems with isabelle make on Windows/Cygwin



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 | \
-  { read FPID; "$POLY" -q $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
+  { read FPID; "$POLY" -q $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
 RC="$?"


      Which means it is just "kill -TERM" instead of "kill -HUP" in the
      feeder script that is wrapped around poly.


	Makarius






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