INSTALL
changeset 17547 b0d70cf4ed18
parent 16653 c12c2f411f77
child 24797 3bc50959c7f0
equal deleted inserted replaced
17546:07371b92d382 17547:b0d70cf4ed18
    15 Ready-to-go packages are provided for the ML compiler and runtime
    15 Ready-to-go packages are provided for the ML compiler and runtime
    16 system, the Isabelle sources, and some major object-logics.  A minimal
    16 system, the Isabelle sources, and some major object-logics.  A minimal
    17 site installation of Isabelle on Linux/x86 works like this:
    17 site installation of Isabelle on Linux/x86 works like this:
    18 
    18 
    19   tar -C /usr/local -xzf Isabelle.tar.gz
    19   tar -C /usr/local -xzf Isabelle.tar.gz
    20   tar -C /usr/local -xzf polyml_base.tar.gz
       
    21   tar -C /usr/local -xzf polyml_x86-linux.tar.gz
    20   tar -C /usr/local -xzf polyml_x86-linux.tar.gz
    22   tar -C /usr/local -xzf HOL_x86-linux.tar.gz
    21   tar -C /usr/local -xzf HOL_x86-linux.tar.gz
    23 
    22 
    24 The install prefix given above may be changed as appropriate.  By
    23 The install prefix given above may be changed as appropriate.  By
    25 default the ML system (and other contributed packages) are expected in
    24 default the ML system (and other contributed packages) are expected in
    26 any of the following locations:
    25 any of the following locations:
    27 
    26 
    28   1) [ISABELLE_HOME]/contrib
    27   1) [ISABELLE_HOME]/contrib
    29   2) [ISABELLE_HOME]/..
    28   2) [ISABELLE_HOME]/..
       
    29   4) /usr/local
    30   3) /usr/share
    30   3) /usr/share
    31   4) /usr/local
       
    32   5) /opt
    31   5) /opt
    33 
    32 
    34 This may be changed by editing [ISABELLE_HOME]/etc/settings manually.
    33 This may be changed by editing [ISABELLE_HOME]/etc/settings manually.
    35 
    34 
    36 The installation may be finished as follows:
    35 The installation may be finished as follows:
    47 
    46 
    48 Compiling logics
    47 Compiling logics
    49 ----------------
    48 ----------------
    50 
    49 
    51 The Isabelle.tar.gz archive already contains all Isabelle sources (and
    50 The Isabelle.tar.gz archive already contains all Isabelle sources (and
    52 documentation). Precompiled object-logics are provided for
    51 documentation).  Precompiled object-logics are provided for
    53 convenience.
    52 convenience.
    54 
    53 
    55 Assuming proper configuration of the underlying ML system
    54 Assuming proper configuration of the underlying ML system
    56 (cf. Isabelle's etc/settings), further object-logics may be compiled
    55 (cf. Isabelle's etc/settings), further object-logics may be compiled
    57 like this:
    56 like this:
    58 
    57 
    59   [ISABELLE_HOME]/build FOL
    58   [ISABELLE_HOME]/build FOL
    60 
    59 
    61 Special object-logic targets may be specified as follows:
    60 Special object-logic targets may be specified as follows:
    62 
    61 
    63   [ISABELLE_HOME]/build -m HOL-Complex HOL
    62   [ISABELLE_HOME]/build -m HOL-Algebra HOL
    64 
    63 
    65 
    64 
    66 2) User installation
    65 2) User installation
    67 --------------------
    66 --------------------
    68 
    67