etc/settings
changeset 14461 fab539f843d9
parent 14451 2253d273d944
child 14613 f0e4b502a208
equal deleted inserted replaced
14460:04e787a4f17a 14461:fab539f843d9
    12 
    12 
    13 # Note that ML_HOME specifies the location of the actual compiler
    13 # Note that ML_HOME specifies the location of the actual compiler
    14 # binaries.  Do not invent new ML system names unless you know what
    14 # binaries.  Do not invent new ML system names unless you know what
    15 # you are doing.  Only one of the sections below should be activated.
    15 # you are doing.  Only one of the sections below should be activated.
    16 
    16 
    17 # Poly/ML 3.x, 4.0, 4.1, 4.1.1, 4.1.2
    17 
    18 if [ -e /usr/bin/poly -a -e /usr/lib/poly ]; then
    18 # try finding the poly packages from the Isabelle site in the usual places
    19   #maybe a shrink-wrapped polyml on x86-linux ...
    19 POLYML_HOME=$(choosefrom \
    20 
    20   "$ISABELLE_HOME/contrib/polyml" \
       
    21   "$ISABELLE_HOME/../polyml" \
       
    22   "/usr/share/polyml" \
       
    23   "/usr/local/polyml" \
       
    24   "/opt/polyml")
       
    25 
       
    26 if [ -n "$POLYML_HOME" -a -e "$POLYML_HOME/bin/polyml-version" ]; then
       
    27   # looks like Isabelle poly packages
       
    28   ML_SYSTEM=$("$POLYML_HOME/bin/polyml-version" 2>/dev/null || echo polyml)
       
    29   ML_PLATFORM=$("$POLYML_HOME/bin/polyml-platform" 2>/dev/null || echo unknown-platform)
       
    30   ML_HOME="$POLYML_HOME/$ML_PLATFORM"
       
    31   ML_OPTIONS="-h 15000"
       
    32 elif [ -e /usr/bin/poly -a -e /usr/lib/poly ]; then
       
    33   # maybe a shrink-wrapped polyml on x86-linux ...
       
    34 
       
    35   # Poly/ML 3.x, 4.0, 4.1, 4.1.x
    21   # include version number, needed for choosing right options
    36   # include version number, needed for choosing right options
    22   ML_SYSTEM=polyml-4.1.3    
    37   ML_SYSTEM=polyml-4.1.3    
    23   # processor/OS type
    38   # processor/OS type
    24   ML_PLATFORM=x86-linux
    39   ML_PLATFORM=x86-linux
    25   # where to find binaries
    40   # where to find binaries
    26   ML_HOME=/usr/bin
    41   ML_HOME=/usr/bin
    27   # where to find the standard database
    42   # where to find the standard database
    28   ML_DBASE=/usr/lib/poly/ML_dbase
    43   ML_DBASE=/usr/lib/poly/ML_dbase
    29   # options to pass to poly
    44   # options to pass to poly
    30   ML_OPTIONS="-h 15000"
    45   ML_OPTIONS="-h 15000"
    31 else
       
    32   #... or rather a self-contained multi-platform installation
       
    33   POLYML_HOME=$(choosefrom \
       
    34     "$ISABELLE_HOME/contrib/polyml" \
       
    35     "$ISABELLE_HOME/../polyml" \
       
    36     "/usr/share/polyml" \
       
    37     "/usr/local/polyml" \
       
    38     "/opt/polyml")
       
    39   ML_SYSTEM=$("$POLYML_HOME/bin/polyml-version" 2>/dev/null || echo polyml)
       
    40   ML_PLATFORM=$("$POLYML_HOME/bin/polyml-platform" 2>/dev/null || echo unknown-platform)
       
    41   ML_HOME="$POLYML_HOME/$ML_PLATFORM"
       
    42   ML_OPTIONS="-h 15000"
       
    43 fi
    46 fi
    44 
    47 
    45 # Standard ML of New Jersey 110 or later
    48 # Standard ML of New Jersey 110 or later
    46 #ML_SYSTEM=smlnj-110
    49 #ML_SYSTEM=smlnj-110
    47 #ML_HOME="$ISABELLE_HOME/../smlnj/bin"
    50 #ML_HOME="$ISABELLE_HOME/../smlnj/bin"