INSTALL
changeset 10029 b889474af53f
parent 9927 7a9652294fe0
child 10038 839340b78fc8
     1.1 --- a/INSTALL	Mon Sep 18 23:59:53 2000 +0200
     1.2 +++ b/INSTALL	Tue Sep 19 23:50:43 2000 +0200
     1.3 @@ -42,11 +42,12 @@
     1.4  
     1.5    [ISABELLE_HOME]/bin/isatool install -k
     1.6  
     1.7 -Clicking on that icon will invoke the interface wrapper script
     1.8 -(capital Isabelle), which may be configured to run your favorite
     1.9 -Isabelle user interface via the ISABELLE_INTERFACE setting.
    1.10 -Additional options may be passed by editing the application's command
    1.11 -line (by using the standard KDE desktop functionality).
    1.12 +You may have to refresh the KDE desktop in order to see the new icon.
    1.13 +Clicking on Isabelle will invoke the interface wrapper script (capital
    1.14 +Isabelle), which is usually configured to run Proof General (see also
    1.15 +the ISABELLE_INTERFACE setting).  Additional options may be passed to
    1.16 +Isabelle by editing the application's command line using the standard
    1.17 +KDE desktop functionality.
    1.18  
    1.19  
    1.20  2) System installation
    1.21 @@ -64,17 +65,25 @@
    1.22  
    1.23  Ready-to-go RPM packages are provided for the ML compiler and runtime
    1.24  system, the Isabelle sources, and some major object-logics.  These
    1.25 -packages should work on any major RPM-based Linux/x86 platform (such
    1.26 -as SuSE, RedHat etc.).  A typical installation procedure would be like
    1.27 -this (executed as root):
    1.28 +packages should work on any major Linux/x86 platform based on RPM
    1.29 +package management.
    1.30  
    1.31 -  rpm -i --prefix /usr/share polyml.i386.rpm
    1.32 -  rpm -i --prefix /usr/share isabelle.rpm
    1.33 -  rpm -i --prefix /usr/share isabelle-HOL.i386.rpm
    1.34 +A minimal installation would work like this (executed as root):
    1.35 +
    1.36 +  rpm -i --force --prefix /usr/share polyml.i386.rpm
    1.37 +  rpm -i --force --prefix /usr/share isabelle.rpm
    1.38 +  rpm -i --force --prefix /usr/share isabelle-HOL.i386.rpm
    1.39  
    1.40  The install prefix may be changed as indicated.  By default the ML
    1.41 -system is expected to be at the same directory level as Isabelle
    1.42 -itself; see [ISABELLE_HOME]/etc/settings of how to change this.
    1.43 +system (and other contributed packages) are expected in either of the
    1.44 +following three locations:
    1.45 +
    1.46 +  1) [ISABELLE_HOME]/contrib
    1.47 +  2) [ISABELLE_HOME]/..
    1.48 +  3) /usr/share
    1.49 +  4) /usr/local
    1.50 +
    1.51 +This may be changed by editing [ISABELLE_HOME]/etc/settings manually.
    1.52  
    1.53  Note that isabelle.rpm and isabelle-pdfdocs.rpm already contain all of
    1.54  Isabelle as platform independent sources.  Precompiled object-logics
    1.55 @@ -85,10 +94,10 @@
    1.56  ------------------
    1.57  
    1.58  Some people prefer to be able to reconstruct the full system from the
    1.59 -sources, rather than installing RPM packages blindly.  We do not
    1.60 -provide source RPMs, yet any parts of Isabelle may be recompiled after
    1.61 -installation of the main isabelle.rpm package (which contains only
    1.62 -sources anyway).
    1.63 +sources, rather than installing precompiled packages blindly.  We do
    1.64 +not provide source RPMs, yet any parts of Isabelle may be recompiled
    1.65 +after installation of the main isabelle.rpm package (which contains
    1.66 +only sources anyway).
    1.67  
    1.68  Assuming proper configuration of the underlying ML system, Isabelle
    1.69  object-logics may be recompiled like this:
    1.70 @@ -100,19 +109,16 @@
    1.71  -------------------
    1.72  
    1.73  Traditional tar.gz archives are provided for the full Isabelle sources
    1.74 -and documentation as well.  Make sure your ML system (SML/NJ, Poly/ML
    1.75 +and documentation as well.  Make sure your ML system (e.g. Poly/ML
    1.76  etc.) has already been installed properly; then proceed as follows.
    1.77  
    1.78  * Unpacking the archives.  After unpacking the Isabelle distribution
    1.79  archives (using tar and gzip) you are left with some directory
    1.80 -IsabelleYY-X.  Basically, this may be installed anywhere --- just note
    1.81 -that ~/isabelle would be a really bad idea, though.  The place where
    1.82 -you put the contents of IsabelleYY-X will be referred to as
    1.83 -[ISABELLE_HOME] subsequently.
    1.84 +IsabelleYY-X.
    1.85  
    1.86  * Auto configuration.  There are some minor adaptions to be made of
    1.87 -the Isabelle distribution to your system environment (mostly locations
    1.88 -of bash and perl).  Simply do it like this:
    1.89 +the Isabelle distribution to your system environment (locations of
    1.90 +bash and perl).  Simply do it like this:
    1.91  
    1.92    cd [ISABELLE_HOME]
    1.93    ./configure