Admin/mira.py
changeset 46200 4a892432e8f1
parent 45164 13dddf30c792
child 46931 d2b92739038b
equal deleted inserted replaced
46199:9d2273d50f4f 46200:4a892432e8f1
   199 
   199 
   200 
   200 
   201 def isabelle_makeall(env, case, paths, dep_paths, playground, usedir_options=default_usedir_options,
   201 def isabelle_makeall(env, case, paths, dep_paths, playground, usedir_options=default_usedir_options,
   202   more_settings='', target='all', make_options=()):
   202   more_settings='', target='all', make_options=()):
   203 
   203 
   204     # FIXME!?
       
   205     if 'lxbroy10' in misc.hostnames():
   204     if 'lxbroy10' in misc.hostnames():
   206         make_options += ('-j', '8')
   205         make_options += ('-j', '8')
   207         usedir_options += " -M 6 -q 2 -i false -d false"
   206         usedir_options += " -M 4 -q 2 -i false -d false"
   208         more_settings += '''
   207         more_settings += '''
   209 ML_PLATFORM="x86_64-linux"
   208 ML_PLATFORM="x86_64-linux"
   210 ML_HOME="/home/polyml/polyml-5.4.1/x86_64-linux"
   209 ML_HOME="/home/polyml/polyml-5.4.1/x86_64-linux"
   211 ML_SYSTEM="polyml-5.4.1"
   210 ML_SYSTEM="polyml-5.4.1"
   212 ML_OPTIONS="-H 8000 --gcthreads 6"
   211 ML_OPTIONS="-H 4000 --gcthreads 4"
   213 
   212 
   214 ISABELLE_GHC="/usr/bin/ghc"
   213 ISABELLE_GHC="/usr/bin/ghc"
   215 '''
   214 '''
   216 
   215 
   217     isabelle_home = paths[0]
   216     isabelle_home = paths[0]