less ambitious isatest, avoid "Exception- InternalError: Backing up too far (32bit) raised while compiling" in polyml-5.4.1;
authorwenzelm
Thu, 24 Jul 2014 14:56:30 +0200
changeset 58988da26d2d6346c
parent 58987 ee55e667dedc
child 58989 5c600dd17617
less ambitious isatest, avoid "Exception- InternalError: Backing up too far (32bit) raised while compiling" in polyml-5.4.1;
Admin/isatest/settings/mac-poly64-M4
Admin/isatest/settings/mac-poly64-M8
     1.1 --- a/Admin/isatest/settings/mac-poly64-M4	Thu Jul 24 14:08:29 2014 +0200
     1.2 +++ b/Admin/isatest/settings/mac-poly64-M4	Thu Jul 24 14:56:30 2014 +0200
     1.3 @@ -8,7 +8,8 @@
     1.4    ML_HOME="$POLYML_HOME/$ML_PLATFORM"
     1.5    ML_OPTIONS="-H 2000 --gcthreads 4"
     1.6  
     1.7 -ISABELLE_GHC=ghc
     1.8 +#FIXME disabled due to polyml-5.4.1 compiler crash in Quickcheck_Lattice_Examples.thy
     1.9 +#ISABELLE_GHC=ghc
    1.10  
    1.11  ISABELLE_HOME_USER=~/isabelle-mac-poly64-M4
    1.12  
     2.1 --- a/Admin/isatest/settings/mac-poly64-M8	Thu Jul 24 14:08:29 2014 +0200
     2.2 +++ b/Admin/isatest/settings/mac-poly64-M8	Thu Jul 24 14:56:30 2014 +0200
     2.3 @@ -8,7 +8,8 @@
     2.4    ML_HOME="$POLYML_HOME/$ML_PLATFORM"
     2.5    ML_OPTIONS="-H 2000 --gcthreads 8"
     2.6  
     2.7 -ISABELLE_GHC=ghc
     2.8 +#FIXME disabled due to polyml-5.4.1 compiler crash in Quickcheck_Lattice_Examples.thy
     2.9 +#ISABELLE_GHC=ghc
    2.10  
    2.11  ISABELLE_HOME_USER=~/isabelle-mac-poly64-M8
    2.12