1.1 --- a/Admin/mira.py	Thu Mar 24 23:35:49 2011 +0100
     1.2 +++ b/Admin/mira.py	Thu Mar 24 23:42:06 2011 +0100
     1.3 @@ -329,3 +329,22 @@
     1.4      """Judgement Day regression suite SN"""
     1.5      return judgement_day('Isabelle/src/HOL/Proofs/Lambda', 'StrongNorm', 'prover_timeout=10', *args)
     1.6  
     1.7 +
     1.8 +# SML/NJ
     1.9 +
    1.10 +smlnj_settings = '''
    1.11 +ML_SYSTEM=smlnj
    1.12 +ML_HOME="/home/smlnj/110.72/bin"
    1.13 +ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=256"
    1.14 +ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
    1.15 +'''
    1.16 +
    1.17 +@configuration(repos = [Isabelle], deps = [])
    1.18 +def SML_HOL(*args):
    1.19 +    """HOL image built with SML/NJ"""
    1.20 +    return isabelle_make('src/HOL', *args, more_settings=smlnj_settings, target='HOL')
    1.21 +
    1.22 +@configuration(repos = [Isabelle], deps = [])
    1.23 +def SML_makeall(*args):
    1.24 +    """Makeall built with SML/NJ"""
    1.25 +    return isabelle_makeall(*args, more_settings=smlnj_settings)