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