INSTALL
author wenzelm
Wed Sep 20 14:59:19 2000 +0200 (2000-09-20)
changeset 10038 839340b78fc8
parent 10029 b889474af53f
child 10081 352412857003
permissions -rw-r--r--
tuned rpm command lines;
wenzelm@2759
     1
wenzelm@8809
     2
Isabelle installation and compilation notes
wenzelm@6486
     3
===========================================
wenzelm@2759
     4
wenzelm@8809
     5
1) User installation
wenzelm@8809
     6
--------------------
wenzelm@8809
     7
wenzelm@8809
     8
Here we assume that Isabelle has already been installed at your site.
wenzelm@8809
     9
Otherwise see 2) below of how to get the Isabelle system installed in
wenzelm@8809
    10
the first place.
wenzelm@8809
    11
wenzelm@8809
    12
wenzelm@8809
    13
1a) Running the Isabelle binaries
wenzelm@8809
    14
---------------------------------
wenzelm@8809
    15
wenzelm@8809
    16
The Isabelle binaries (isatool, isabelle, Isabelle) may be invoked
wenzelm@8809
    17
directly from their location within the distribution directory
wenzelm@8809
    18
[ISABELLE_HOME] like this:
wenzelm@8809
    19
wenzelm@8809
    20
  [ISABELLE_HOME]/bin/isabelle HOL
wenzelm@8809
    21
wenzelm@8809
    22
This starts an interactive Isabelle session within your current text
wenzelm@8809
    23
terminal.  You may want to put [ISABELLE_HOME]/bin into your shell's
wenzelm@8809
    24
search PATH, but this is not strictly necessary.
wenzelm@8809
    25
wenzelm@8809
    26
wenzelm@8809
    27
Please do *not* copy (or link) the Isabelle scripts anywhere else ---
wenzelm@8809
    28
they just won't work!  If you really want to install independent
wenzelm@8809
    29
Isabelle binaries somewhere else then do it like this:
wenzelm@8809
    30
wenzelm@8809
    31
  [ISABELLE_HOME]/bin/isatool install -p ~/bin
wenzelm@2759
    32
wenzelm@8809
    33
Your site-wide Isabelle installation may already provide Isabelle
wenzelm@8809
    34
executables in some global bin directory (such as /usr/bin).
wenzelm@8809
    35
wenzelm@8809
    36
wenzelm@8809
    37
1b) Isabelle as KDE application
wenzelm@8809
    38
-------------------------------
wenzelm@8809
    39
wenzelm@8809
    40
Isabelle may be installed as application icon on the KDE desktop like
wenzelm@8809
    41
this:
wenzelm@8809
    42
wenzelm@8809
    43
  [ISABELLE_HOME]/bin/isatool install -k
wenzelm@2759
    44
wenzelm@10029
    45
You may have to refresh the KDE desktop in order to see the new icon.
wenzelm@10029
    46
Clicking on Isabelle will invoke the interface wrapper script (capital
wenzelm@10029
    47
Isabelle), which is usually configured to run Proof General (see also
wenzelm@10029
    48
the ISABELLE_INTERFACE setting).  Additional options may be passed to
wenzelm@10029
    49
Isabelle by editing the application's command line using the standard
wenzelm@10029
    50
KDE desktop functionality.
wenzelm@8809
    51
wenzelm@8809
    52
wenzelm@8809
    53
2) System installation
wenzelm@8809
    54
----------------------
wenzelm@8809
    55
wenzelm@8809
    56
The Isabelle distribution is available both as traditional source-only
wenzelm@8809
    57
tar.gz archives, and as binary packages (currently only RPM for
wenzelm@8809
    58
Linux/x86).  In any case, the resulting Isabelle installation always
wenzelm@8809
    59
contains the full sources, thus any part of the system be recompiled
wenzelm@8809
    60
later, too.
wenzelm@2759
    61
wenzelm@2759
    62
wenzelm@8809
    63
2a) Binary installation
wenzelm@8809
    64
----------------------
wenzelm@8809
    65
wenzelm@8809
    66
Ready-to-go RPM packages are provided for the ML compiler and runtime
wenzelm@8809
    67
system, the Isabelle sources, and some major object-logics.  These
wenzelm@10029
    68
packages should work on any major Linux/x86 platform based on RPM
wenzelm@10029
    69
package management.
wenzelm@8809
    70
wenzelm@10029
    71
A minimal installation would work like this (executed as root):
wenzelm@10029
    72
wenzelm@10038
    73
  rpm -i --prefix /usr/share polyml.i386.rpm
wenzelm@10038
    74
  rpm -i --prefix /usr/share isabelle.rpm
wenzelm@10038
    75
  rpm -i --prefix /usr/share isabelle-HOL.i386.rpm
wenzelm@8809
    76
wenzelm@10038
    77
Note that installed RPMs may be removed like this:
wenzelm@10038
    78
wenzelm@10038
    79
  rpm -e isabelle-HOL isabelle polyml
wenzelm@10038
    80
wenzelm@10038
    81
The install prefix given above may be changed.  By default the ML
wenzelm@10029
    82
system (and other contributed packages) are expected in either of the
wenzelm@10029
    83
following three locations:
wenzelm@10029
    84
wenzelm@10029
    85
  1) [ISABELLE_HOME]/contrib
wenzelm@10029
    86
  2) [ISABELLE_HOME]/..
wenzelm@10029
    87
  3) /usr/share
wenzelm@10029
    88
  4) /usr/local
wenzelm@10029
    89
wenzelm@10038
    90
This may be changed further by editing [ISABELLE_HOME]/etc/settings
wenzelm@10038
    91
manually.
wenzelm@8809
    92
wenzelm@8809
    93
Note that isabelle.rpm and isabelle-pdfdocs.rpm already contain all of
wenzelm@8809
    94
Isabelle as platform independent sources.  Precompiled object-logics
wenzelm@8809
    95
are provided for convenience.
wenzelm@8809
    96
wenzelm@8809
    97
wenzelm@8809
    98
Recompiling logics
wenzelm@3263
    99
------------------
wenzelm@2759
   100
wenzelm@8809
   101
Some people prefer to be able to reconstruct the full system from the
wenzelm@10029
   102
sources, rather than installing precompiled packages blindly.  We do
wenzelm@10029
   103
not provide source RPMs, yet any parts of Isabelle may be recompiled
wenzelm@10029
   104
after installation of the main isabelle.rpm package (which contains
wenzelm@10029
   105
only sources anyway).
wenzelm@8809
   106
wenzelm@8809
   107
Assuming proper configuration of the underlying ML system, Isabelle
wenzelm@8809
   108
object-logics may be recompiled like this:
wenzelm@8809
   109
wenzelm@8809
   110
  [ISABELLE_HOME]/build HOL FOL
wenzelm@8809
   111
wenzelm@8809
   112
wenzelm@8809
   113
Source installation
wenzelm@8809
   114
-------------------
wenzelm@8809
   115
wenzelm@8809
   116
Traditional tar.gz archives are provided for the full Isabelle sources
wenzelm@10029
   117
and documentation as well.  Make sure your ML system (e.g. Poly/ML
wenzelm@8809
   118
etc.) has already been installed properly; then proceed as follows.
wenzelm@8809
   119
wenzelm@8809
   120
* Unpacking the archives.  After unpacking the Isabelle distribution
wenzelm@8809
   121
archives (using tar and gzip) you are left with some directory
wenzelm@10029
   122
IsabelleYY-X.
wenzelm@8809
   123
wenzelm@8809
   124
* Auto configuration.  There are some minor adaptions to be made of
wenzelm@10029
   125
the Isabelle distribution to your system environment (locations of
wenzelm@10029
   126
bash and perl).  Simply do it like this:
wenzelm@2759
   127
wenzelm@2759
   128
  cd [ISABELLE_HOME]
wenzelm@2759
   129
  ./configure
wenzelm@2759
   130
wenzelm@8809
   131
Note that this does not store any references to [ISABELLE_HOME].  You
wenzelm@8809
   132
may safely move the system later, without having to run ./configure
wenzelm@8809
   133
again.
wenzelm@6258
   134
wenzelm@8809
   135
* ML system settings and compilation.  Before actual compilation you
wenzelm@8809
   136
have to tell Isabelle about your Standard ML system.  These settings
wenzelm@8809
   137
reside in ./etc/settings, which may be also overridden by
wenzelm@8809
   138
~/isabelle/etc/settings. There are already various sample
wenzelm@8809
   139
configurations in ./etc/settings commented out.
wenzelm@2759
   140
wenzelm@3117
   141
To build the core Isabelle/Pure and the default object-logic, just
wenzelm@8809
   142
type
wenzelm@2759
   143
wenzelm@2759
   144
  ./build
wenzelm@2759
   145
wenzelm@8809
   146
More object-logics can be made in a similar fashion:
wenzelm@2759
   147
wenzelm@2759
   148
  ./build FOL HOL
wenzelm@2759
   149
wenzelm@9927
   150
Explicit make targets may be given as follows:
wenzelm@9927
   151
wenzelm@9927
   152
  ./build -m HOL-Real HOL
wenzelm@9927
   153
wenzelm@8809
   154
After successful compilation you are ready to run the system, see 1)
wenzelm@8809
   155
above for more information.
wenzelm@2759
   156
wenzelm@2759
   157
wenzelm@2759
   158
$Id$