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



Hi Makarius,

Inbetween I was able to get the system document preparation working fine
in linux mint 13 installed into a virtual machine.

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?), 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;

Best!

In the "Prover Session / Syslog" there was only this message:

On Wed, Oct 10, 2012 at 3:08 PM, Makarius <makarius at sketis.net> wrote:

> 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:
>
> ec5d5402966416bc2656e9d100e287**c208555361 Isabelle2012-RC1
> 1636ff4c6243b653054e3061d312f7**859c67429c Isabelle2012-RC2
> ed5f56b8f90ae33ffa10b6eadee2f9**433bddc5eb 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<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
>
>


-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil




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