etc/settings
changeset 25347 297e2520ee82
parent 25115 ec2498132ac4
child 25500 7a284dc85326
equal deleted inserted replaced
25346:7f2e3292e3dd 25347:297e2520ee82
    28   $POLY_HOME)
    28   $POLY_HOME)
    29 ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version")
    29 ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version")
    30 ML_OPTIONS="-H 500"
    30 ML_OPTIONS="-H 500"
    31 ML_DBASE=""
    31 ML_DBASE=""
    32 
    32 
    33 # Poly/ML 5.1 on 64bit Linux
    33 # Poly/ML 5.1
       
    34 #ML_PLATFORM=x86-linux
       
    35 #ML_HOME=/usr/local/polyml/x86-linux
       
    36 #ML_SYSTEM=polyml-5.1
       
    37 #ML_OPTIONS="-H 500"
       
    38 
       
    39 # Poly/ML 5.1 (64 bit)
    34 #ML_PLATFORM=x86_64-linux
    40 #ML_PLATFORM=x86_64-linux
    35 #ML_HOME=/usr/local/polyml/x86_64-linux
    41 #ML_HOME=/usr/local/polyml/x86_64-linux
    36 #ML_SYSTEM=polyml-5.1
    42 #ML_SYSTEM=polyml-5.1
    37 #ML_OPTIONS="-H 1000"
    43 #ML_OPTIONS="-H 1000"
    38 
       
    39 # Poly/ML 5.1 on Cygwin
       
    40 #ML_PLATFORM=x86-cygwin
       
    41 #ML_HOME=/usr/local/polyml/x86-cygwin
       
    42 #ML_SYSTEM=polyml-5.1
       
    43 #ML_OPTIONS="-H 500"
       
    44 #POLY_LINK_OPTIONS="-lstdc++"
       
    45 
    44 
    46 # Poly/ML 4.2.0
    45 # Poly/ML 4.2.0
    47 #ML_PLATFORM=x86-linux
    46 #ML_PLATFORM=x86-linux
    48 #ML_HOME=/usr/local/polyml/x86-linux
    47 #ML_HOME=/usr/local/polyml/x86-linux
    49 #ML_SYSTEM=polyml-4.2.0
    48 #ML_SYSTEM=polyml-4.2.0
    50 #ML_OPTIONS="-H 80"
    49 #ML_OPTIONS="-H 80"
    51 
    50 
    52 # Standard ML of New Jersey 110 or later
    51 # Standard ML of New Jersey (slow!)
    53 #SMLNJ_CYGWIN_RUNTIME=1
       
    54 #ML_SYSTEM=smlnj-110
    52 #ML_SYSTEM=smlnj-110
    55 #ML_HOME="$ISABELLE_HOME/contrib/smlnj/bin"
    53 #ML_HOME="/usr/local/smlnj/bin"
    56 #ML_OPTIONS="@SMLdebug=/dev/null"
    54 #ML_OPTIONS="@SMLdebug=/dev/null"
    57 #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
    55 #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
    58 
    56 #SMLNJ_CYGWIN_RUNTIME=1
    59 # Moscow ML 2.00 or later (experimental!)
    57 
       
    58 # Moscow ML 2.00 (experimental!)
    60 #ML_SYSTEM=mosml
    59 #ML_SYSTEM=mosml
    61 #ML_HOME="$ISABELLE_HOME/contrib/mosml/bin"
    60 #ML_HOME="/usr/local/mosml/bin"
       
    61 #ML_OPTIONS=""
       
    62 #ML_PLATFORM=""
       
    63 
       
    64 # Alice 1.4 (experimental!)
       
    65 #ML_SYSTEM=alice
       
    66 #ML_HOME="/usr/local/alice/bin"
    62 #ML_OPTIONS=""
    67 #ML_OPTIONS=""
    63 #ML_PLATFORM=""
    68 #ML_PLATFORM=""
    64 
    69 
    65 # Poplog/PML version 15.6/2.1 (experimental!)
    70 # Poplog/PML version 15.6/2.1 (experimental!)
    66 #ML_SYSTEM=poplogml
    71 #ML_SYSTEM=poplogml
    67 #ML_HOME="/usr/local/poplog/current-poplog/bin"
    72 #ML_HOME="/usr/local/poplog/current-poplog/bin"
    68 #ML_OPTIONS="-noinit"
    73 #ML_OPTIONS="-noinit"
    69 #ML_SUFFIX=".psv"
    74 #ML_SUFFIX=".psv"
    70 #ML_PLATFORM=""
       
    71 
       
    72 # Alice 1.4 (experimental!)
       
    73 #ML_SYSTEM=alice
       
    74 #ML_HOME="/usr/local/alice/bin"
       
    75 #ML_OPTIONS=""
       
    76 #ML_PLATFORM=""
    75 #ML_PLATFORM=""
    77 
    76 
    78 
    77 
    79 ###
    78 ###
    80 ### Compilation options (cf. isatool usedir)
    79 ### Compilation options (cf. isatool usedir)