etc/settings
changeset 9787 fb8c5a66dbe8
parent 9759 8e835ebc862f
child 9818 71de955e8fc9
equal deleted inserted replaced
9786:270ca580b880 9787:fb8c5a66dbe8
    21   "$ISABELLE_HOME/../polyml-3.x" \
    21   "$ISABELLE_HOME/../polyml-3.x" \
    22   "$ISABELLE_HOME/../polyml" \
    22   "$ISABELLE_HOME/../polyml" \
    23   "/usr/share/polyml-4.0" \
    23   "/usr/share/polyml-4.0" \
    24   "/usr/share/polyml-3.x" \
    24   "/usr/share/polyml-3.x" \
    25   "/usr/share/polyml")
    25   "/usr/share/polyml")
    26 ML_SYSTEM=$($POLYML_HOME/bin/polyml-version 2>/dev/null || echo polyml)
    26 ML_SYSTEM=$("$POLYML_HOME/bin/polyml-version" 2>/dev/null || echo polyml)
    27 ML_PLATFORM=$($POLYML_HOME/bin/polyml-platform 2>/dev/null)
    27 ML_PLATFORM=$("$POLYML_HOME/bin/polyml-platform" 2>/dev/null)
    28 ML_HOME=$POLYML_HOME/$ML_PLATFORM
    28 ML_HOME="$POLYML_HOME/$ML_PLATFORM"
    29 ML_OPTIONS="-h 30000"
    29 ML_OPTIONS="-h 30000"
    30 
    30 
    31 # Standard ML of New Jersey 110 or later
    31 # Standard ML of New Jersey 110 or later
    32 #ML_SYSTEM=smlnj-110
    32 #ML_SYSTEM=smlnj-110
    33 #ML_HOME=$ISABELLE_HOME/../smlnj/bin
    33 #ML_HOME="$ISABELLE_HOME/../smlnj/bin"
    34 #ML_OPTIONS="@SMLdebug=/dev/null"
    34 #ML_OPTIONS="@SMLdebug=/dev/null"
    35 #ML_PLATFORM=$(eval $($ML_HOME/.arch-n-opsys 2>/dev/null); echo $HEAP_SUFFIX)
    35 #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
    36 
    36 
    37 # Moscow ML 2.00 or later (experimental!)
    37 # Moscow ML 2.00 or later (experimental!)
    38 #ML_SYSTEM=mosml
    38 #ML_SYSTEM=mosml
    39 #ML_HOME=$ISABELLE_HOME/../mosml/bin
    39 #ML_HOME="$ISABELLE_HOME/../mosml/bin"
    40 #ML_PLATFORM=""
    40 #ML_PLATFORM=""
    41 #ML_OPTIONS=""
    41 #ML_OPTIONS=""
    42 
    42 
    43 # MLWorks 2.0
    43 # MLWorks 2.0
    44 #ML_SYSTEM=mlworks
    44 #ML_SYSTEM=mlworks
    45 #ML_HOME=$ISABELLE_HOME/../mlworks/bin
    45 #ML_HOME="$ISABELLE_HOME/../mlworks/bin"
    46 #ML_OPTIONS=""
    46 #ML_OPTIONS=""
    47 #ML_PLATFORM=""
    47 #ML_PLATFORM=""
    48 
    48 
    49 # Standard ML of New Jersey 0.93
    49 # Standard ML of New Jersey 0.93
    50 #ML_SYSTEM=smlnj-0.93
    50 #ML_SYSTEM=smlnj-0.93
    81 
    81 
    82 # The place for user configuration, heap files, etc.
    82 # The place for user configuration, heap files, etc.
    83 ISABELLE_HOME_USER=~/isabelle
    83 ISABELLE_HOME_USER=~/isabelle
    84 
    84 
    85 # Where to look for isabelle tools (multiple dirs separated by ':').
    85 # Where to look for isabelle tools (multiple dirs separated by ':').
    86 ISABELLE_TOOLS=$ISABELLE_HOME/lib/Tools
    86 ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
    87 
    87 
    88 # Location for temporary files (should be on a local file system).
    88 # Location for temporary files (should be on a local file system).
    89 ISABELLE_TMP_PREFIX=/tmp/isabelle-$USER
    89 ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
    90 
    90 
    91 
    91 
    92 # Heap file locations. ML system identifier appended automatically!
    92 # Heap input locations. ML system identifier is included in lookup.
       
    93 ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
    93 
    94 
    94 ISABELLE_PATH=$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps
    95 # Heap output location. ML system identifier is appended automatically later on.
    95 
       
    96 #A hack! Isabelle build tells us to store heaps etc. within the
       
    97 #distribution.
       
    98 if [ "$THIS_IS_ISABELLE_BUILD" = true ]; then
    96 if [ "$THIS_IS_ISABELLE_BUILD" = true ]; then
    99   ISABELLE_OUTPUT=$ISABELLE_HOME/heaps
    97   #Isabelle build tells us to store heaps etc. within the distribution.
   100   ISABELLE_BROWSER_INFO=$ISABELLE_HOME/browser_info
    98   ISABELLE_OUTPUT="$ISABELLE_HOME/heaps"
       
    99   ISABELLE_BROWSER_INFO="$ISABELLE_HOME/browser_info"
   101 else
   100 else
   102   ISABELLE_OUTPUT=$ISABELLE_HOME_USER/heaps
   101   ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
   103   ISABELLE_BROWSER_INFO=$ISABELLE_HOME_USER/browser_info
   102   ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
   104 fi
   103 fi
   105 
   104 
   106 # Site settings check -- just to make it a little bit harder to copy this file!
   105 # Site settings check -- just to make it a little bit harder to copy this file!
   107 [ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \
   106 [ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \
   108   { echo >&2 "### Isabelle site settings already present!  Maybe copied etc/settings in full?"; }
   107   { echo >&2 "### Isabelle site settings already present!  Maybe copied etc/settings in full?"; }
   112 
   111 
   113 
   112 
   114 ## Docs
   113 ## Docs
   115 
   114 
   116 #Where to look for docs (multiple dirs separated by ':').
   115 #Where to look for docs (multiple dirs separated by ':').
   117 ISABELLE_DOCS=$ISABELLE_HOME/doc
   116 ISABELLE_DOCS="$ISABELLE_HOME/doc"
   118 
   117 
   119 #The dvi file viewer
   118 #The dvi file viewer
   120 DVI_VIEWER=xdvi
   119 DVI_VIEWER=xdvi
   121 #DVI_VIEWER="xdvi -geometry 498x704 -expert -s 5"
   120 #DVI_VIEWER="xdvi -geometry 498x704 -expert -s 5"
   122 #DVI_VIEWER="xdvi -geometry 500x704 -expert -s 10"
   121 #DVI_VIEWER="xdvi -geometry 500x704 -expert -s 10"
   124 
   123 
   125 
   124 
   126 ## Fonts -- how to install the Isabelle X11 fonts (can be tricky!).
   125 ## Fonts -- how to install the Isabelle X11 fonts (can be tricky!).
   127 
   126 
   128 # (1) Get fonts from local (client side) directory:
   127 # (1) Get fonts from local (client side) directory:
   129 ISABELLE_INSTALLFONTS="xset fp+ $ISABELLE_HOME/lib/fonts; xset fp rehash"
   128 ISABELLE_INSTALLFONTS="xset fp+ \"$ISABELLE_HOME/lib/fonts\"; xset fp rehash"
   130 
   129 
   131 # (2) Get from font server at Munich or Cambridge:
   130 # (2) Get from font server at Munich or Cambridge:
   132 #ISABELLE_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"
   131 #ISABELLE_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"
   133 #ISABELLE_INSTALLFONTS="xset fp+ tcp/font-serv.cl.cam.ac.uk:7100"
   132 #ISABELLE_INSTALLFONTS="xset fp+ tcp/font-serv.cl.cam.ac.uk:7100"
   134 
   133 
   144 ISABELLE_INTERFACE=xterm
   143 ISABELLE_INTERFACE=xterm
   145 ISABELLE_XTERM_OPTIONS=""
   144 ISABELLE_XTERM_OPTIONS=""
   146 
   145 
   147 # Emacs running Isamode.
   146 # Emacs running Isamode.
   148 #ISABELLE_INTERFACE=emacs
   147 #ISABELLE_INTERFACE=emacs
   149 ISAMODE_HOME=$ISABELLE_HOME/contrib/Isamode
   148 ISAMODE_HOME="$ISABELLE_HOME/contrib/Isamode"
   150 ISAMODE_OPTIONS=""
   149 ISAMODE_OPTIONS=""
   151 
   150 
   152 # Proof General
   151 # Proof General
   153 ISABELLE_INTERFACE=$(choosefrom \
   152 ISABELLE_INTERFACE=$(choosefrom \
   154   "$ISABELLE_HOME/contrib/ProofGeneral/isar/interface" \
   153   "$ISABELLE_HOME/contrib/ProofGeneral/isar/interface" \
   155   "$ISABELLE_HOME/../ProofGeneral/isar/interface" \
   154   "$ISABELLE_HOME/../ProofGeneral/isar/interface" \
       
   155   "/usr/share/ProofGeneral/isar/interface" \
   156   "$ISABELLE_INTERFACE")
   156   "$ISABELLE_INTERFACE")
   157 PROOFGENERAL_OPTIONS=""
   157 PROOFGENERAL_OPTIONS=""
   158 
   158 
   159 # X-Symbol mode for Proof General
   159 # X-Symbol mode for Proof General
   160 XSYMBOL_HOME=$(choosefrom \
   160 XSYMBOL_HOME=$(choosefrom \
   161   "$ISABELLE_HOME/contrib/x-symbol" \
   161   "$ISABELLE_HOME/contrib/x-symbol" \
   162   "$ISABELLE_HOME/../x-symbol" \
   162   "$ISABELLE_HOME/../x-symbol" \
       
   163   "/usr/share/x-symbol" \
   163   "")
   164   "")
   164 
   165 
   165 
   166 
   166 ###
   167 ###
   167 ### External reasoning tools
   168 ### External reasoning tools