================================================================================
$Header: /home/rda/opp/RCS/README.opp.src,v 1.39 2005/09/21 11:51:53 rda Exp $

This is the README file for the Open ProofPower product suite, version 2.7.6
The open source suite comprises the following five packages:

 PPTex - The ProofPower documentation preparation system
 PPDev - The ProofPower developer toolkit
 PPHol - The ProofPower tools supporting specification and proof in HOL
 PPZed - The ProofPower tools supporting specification and proof in Z
 PPXpp - The X/Motif user interface for ProofPower

See the file LICENSE for your rights to use and modify this software.

A sixth package, PPDaz, is also available under licence from Lemma 1 Ltd.
PPDaz provides the Compliance Tool which supports specification and proof of
Ada code using Z.  Licences are free of charge for commercial evaluation and
for academic and personal use.

See the file CHANGES for changes in this version.

The ProofPower web-site contains further information about ProofPower,
including the documentation suite in PDF format. The ProofPower web-site is at:

        http://www.lemma-one.com/ProofPower/index/index.html

ProofPower is Copyright (c) Lemma 1 Limited 2004.
================================================================================
1. A QUICK GUIDE TO THE INSTALLATION

WHAT YOU WILL NEED:

To install the software you need a system running a UNIX or UNIX-like operating
system such as Solaris, Linux or MacOS X with:

a) an ANSI-C compiler: e.g., gcc
b) Common UNIX utilities (nroff, ed, nl etc.)
c) X Windows and Motif run-time and developer software
d) a Standard ML compiler: either Poly/ML or Standard ML of New Jersey
e) the Tex and LaTeX typesetting software

If you do not have some of the software needed to install ProofPower, see under
SYSTEM REQUIREMENTS below for more information on what is needed and where it
may be obtained.

WHAT YOU DO:

A) Unpack the tarball OpenProofPower-2.7.6.tgz working in an empty directory
of your choice. E.g., 

        mkdir $HOME/pp_bld
        cd $HOME/pp_bld
        gunzip -c </tmp/OpenProofPower-2.7.6.tgz | tar xvf -

B) Run the "configure" script:

        ./configure

The "configure" script selects values for installation parameters such as the
name of directory to use as the ProofPower home directory to hold the installed
software.  It reports on the parameters selected and creates a script "install"
to carry out the installation.  You can specify your choice of installation
parameters when you run configure as described under THE INSTALLATION SCRIPTS
below.

C) If you are happy with the output from "configure", run the install script:

        ./install

This installs the software giving a brief report on what is being done. The
installation process produces some log files, and the report tells you where to
find these in case of errors. See under THE INSTALLATION SCRIPTS below for
more information about controlling install.

The ProofPower software is now installed in the ProofPower home directory,
e.g., "/usr/local/pp". This has subdirectories "bin" containing the binaries,
"doc" containing the documentation and so on.

ProofPower users generally want to have the ProofPower binaries on their search
path so they can run ProofPower without typing in the full path names.  See
under SYSTEM ADMINISTRATION FOR PROOFPOWER below for more information.

The PPTex, PPXpp, PPHol and PPZed packages include UN*X-style manual pages for
the command line interfaces. These are installed as troff source files in the
subdirectory man/man1 of the ProofPower home directory.

Some of the ProofPower documents contain diagrams. If these appear to be missing
when you view the documents, you may need to set the TEXINPUTS environment
variable to tell the DVI browser where to look for the documents (see under
TEXINPUTS below).

If you have problems with installing or using ProofPower, please let us know. A
good way of doing this is via the ProofPower mailing list. See the ProofPower
web-site for more information about the mailing list.

2. SYSTEM REQUIREMENTS

ProofPower has been developed under x86-Linux, Sparc-Solaris 2.X and
PowerPC-Mac OS X.  You may well be able to compile and run it on other UNIX or
UNIX-like (UN*X) platforms. You certainly need:

a) an ANSI-C compiler: e.g., gcc
b) Common UNIX text-processing utilities (nroff, ex, nl etc.)
c) X Windows and Motif run-time and developer software
d) a Standard ML compiler: either Poly/ML or Standard ML of New Jersey
e) the Tex and LaTeX typesetting software

Sections 2.A to 2.E below give more information on these items. These sections
assume you are familiar with the process of downloading and installing open
source software for your system.

When unpacked, the distribution occupies about 17Mb. Compilation of the full
open source distribution increases this to about 150Mb (for Poly/ML) or 250Mb
(for Standard ML of New Jersey). About 100Mb (Poly/ML) or 125Mb (Standard ML of
New Jersey) of this comprises the original source files and various temporary
files and this can be reclaimed if desired.

The time taken by the compilation and installation depends on your hardware and
the compiler you use. E.g., using Poly/ML it takes about 10 minutes on a
notebook with a 798MHz Pentium III CPU and  256Mb of memory; on the same system
using Standard ML of New Jersey it takes about 25 minutes.

2.A C Compiler

The PPTex and PPXpp packages are implemented in ANSI C. The GNU C compiler
(gcc) is recommended. GNU C is available for all Linux distributions. GNU C is
also included in the Darwin Developer Tools supplied with Mac OS X (see
section 0.7 below).

PPXpp does not compile on Solaris with the C compiler provided as part of
Sun's BSD compatibility package.  If you do not have an ANSI C compiler
installed under Solaris, the GNU C compiler may be obtained via:

        http://gcc.gnu.org/

On Mac OS X you need the Darwin Developer Tools. These include gcc and are
supplied with Mac OS X, but are not installed by default. To install them open
the folder /Applications/Installers/Developer Tools, double click on
Developer.mpkg and follow the instructions in the Installer program.

2.B Other UN*X Utilities.

Installation of PPHol, PPXpp and  PPZed uses the ex text editor. The
installation script expects ex to be in a directory on your search path. Under
Linux, ex is supplied with the vi-like text editors such as VIM, Elvis or NVI.

Installation of PPXpp uses the nroff text processor. This is bundled with
Solaris and Mac OS X. It is bundled on some Linux distributions but not all (it
is usually supplied with the distribution, but not always installed by
default).  It is usually supplied in the groff or groff-for-man packages or you
can find it by searching for groff at:

        http://www.gnu.org

Mac OS X does not include some of the text processing utilities that are used
to build ProofPower. The GNU coreutils package provides what is needed and can
be obtained via the GNU website at the above web address.

None of the UN*X utilities mentioned above are needed to use ProofPower once it
has been built and installed.

2.C X Windows and Motif

PPXpp uses X Windows and the Motif library. You need the Motif runtime and
development software at version 2.1 or later. The X Windows software is bundled
with Solaris 2.X, with all common Linux distributions and with MacOS X 10.3 or
later.

LessTif is a Motif clone that is included in some older Linux distributions.
The LessTif developers do intend to make LessTif comply with Motif 2.1.  PPXpp
uses Motif features which are not properly supported by LessTif 0.93.18-5.  If
you have LessTif installed on your system, we recommend you replace it with
Motif implementation such as OpenMotif that complies with the Motif 2.1 or 2.2
specifications.

By default the "configure" script expects Motif to be installed in the standard
directories containing the X Windows software for your system. If your
installation of Motif is not installed in these directories, see under THE
INSTALLATION SCRIPTS below for information on how to work with it.

Solaris:

The Motif runtime and development software is bundled with Solaris 2.X.

Linux & Mac OS X:

The OpenMotif runtime and development software can be downloaded from the
MotifZone web site at:

        http://www.motifzone.org/

2.D Standard ML Compiler

The PPDev, PPHol and PPZed packages are implemented in Standard ML.  Poly/ML at
version 4.1.3 is the recommended Standard ML compiler and may be obtained from:

        http://www.polyml.org

When you install Poly/ML, if you follow the convention of having the Poly/ML
database in /usr/lib/poly/ML_dbase then the "configure" script finds it
automatically.  If your Poly/ML installation does not follow this convention
see under THE INSTALLATION SCRIPTS below for how to work with it.

Standard ML of New Jersey also works well, although for ProofPower it is slower
than Poly/ML and uses more memory and disc space. It may be obtained from:

        http://cm.bell-labs.com/cm/cs/what/smlnj/index.html

ProofPower has been tested using version 110.54 of Standard ML of New
Jersey. It will not compile using earlier versions.

If you are using Standard ML of New Jersey, then you need the bin subdirectory
of its installation directory to be on your path - this directory includes a
script called .arch-n-opsys which is used by some of the scripts in ProofPower.

2.E LaTeX

The ProofPower document preparation system uses the TeX/LaTeX typesetting
software. This comes bundled with most Linux distributions.  The teTeX
implementation of TeX & LaTeX for Linux or Solaris is available from

        http://www.tug.org/tetex/

Tex-Live teTeX for Mac OS X is an easy to install implementation available from:

        http://www.rna.nl/tex.html

If you want the ProofPower documentation in PDF or PostScript format, you need
one of dvipdf, dvipdfm or dvips to do the conversion from the DVI format (see
discussion of PPDOCFORMAT below).  If you do not have these they can be
obtained via:

        http://www.ctan.org

3. THE INSTALLATION SCRIPTS

The "configure" script inspects the environment and various aspects of your
system and uses these to generate a script "install" which actually builds and
installs the software. The scripts are run in the build directory
OpenProofPower-2.7.6 created when you unpack the OpenProofPower tarball.

To run these scripts you need write access to the build directory and to the
directory selected as the ProofPower home directory (see below).  The scripts
do not create or change files other than in these directories and do not
need super-user privileges, unless needed to write to those directories.

3.A THE CONFIGURE SCRIPT

The "configure" script is controlled by parameters that you can set when you
call "./configure".  For example, you can set the parameter PPHOME to specify
your choice for the ProofPower home directory (i.e. the directory where the
ProofPower software is installed) and you can set PPCOMPILER to specify which
Standard ML compiler to use.  Thus to tell "configure" to use /opt/pp-2.7.6
for the ProofPower home directory and to compile using Standard ML of New
Jersey, you would use the following:

        PPHOME=/opt/pp-2.7.6 PPCOMPILER=SMLNJ ./configure

The above example is for the Bourne shell or similar. If you are
using the C shell, the above example would read:

        setenv PPHOME /opt/pp-2.7.6
        setenv PPCOMPILER SMLNJ
        ./configure

The "configure" script selects default values for the parameters that you do
not specify.  For example, the default value for PPHOME is the first of
/usr/local/pp, /usr/share/pp, /opt/pp, /sw/pp and $HOME/pp that looks likely to
work and the default value for PPCOMPILER is whichever of Poly/ML or Standard
ML of New Jersey you have installed (Poly/ML if you have both).  For a complete
list of the parameters and their defaults, see the comments at the top of the
"configure" script.

If you are using Poly/ML you may need to use PPPOLYDBASE to supply the name of
the file containing the Poly/ML compiler database. This defaults to
/usr/lib/poly/ML_dbase, which is appropriate for Poly/ML installed under Linux
using the RPM.  If, for example, you have installed the database in $HOME/lib,
then you would use:

        PPPOLYDBASE=$HOME/lib/ML_dbase ./configure

If Motif is not installed alongside the standard X Windows software on your
system, you can use PPMOTIFHOME to specify the directory in which the Motif
"include" and "lib" directories can be found. For example, if you use Fink to
install Motif on Mac OS X, it will install it in a subdirectory of /sw, rather
than alongside the standard X Windows software in /usr/X11R6. If the build
fails while building PPXpp and the log file "build.log" contains error messages
saying that files with names beginning with "Xm/" cannot be found or that
"-lXm" cannot be found, then you will need to use this parameter.

PPDOCFORMAT may be used to have the documentation converted from DVI format
into PostScript (PPDOCFORMAT=PS) or Portable Document Format (PPDOCFORMAT=PDF).
The configure script generates an HTML file, index.html, in the doc
subdirectory of the installation directory. This HTML file contains links to
the documents in the format you have selected.

WARNING: the configure script tidies up the "src" directory in preparation for
the installation. It attempts to delete any files or directories you have
created in this directory.

3.B THE INSTALL SCRIPT

The "configure" script creates a script called "install" that you use
to compile and install ProofPower in the chosen ProofPower home directory.
For normal installations you simply call "./install". 

The "install" script can be given an option which is useful if you are patching
an existing installation, e.g., to upgrade just one of the packages or to
convert the documents into a new format. The call

        ./install -d

just installs the chosen packages together with the DVI formatted documents
for that package. The call

        ./install +d

just does the document format conversions specified when you ran configure and
generate a new HTML index file.

If you are upgrading one of the packages then run configure using PPTARGETS to
select the package in question and then run install with the -d option. This
gives you the revised versions of any documents for that package in the DVI
format and preserves your existing HTML index file.  If you now want the
documents in a different format, run configure with PPDOCFORMAT set to PS or
PDF as appropriate and with PPTARGETS set to select all the packages you have
installed and then run install with the +d option. This converts all the
documents and regenerates the HTML index file.

If the installation process is successful, you may choose to remove the
OpenProofPower build directory.  If you choose to keep the build directory, you
can save space by tidying up the "src" directory using the script "distclean":

        ./distclean

If the installation fails for some reason, it is generally advisable to call
"./distclean" to tidy up the "src" directory before trying to do the
installation again.

WARNING: the "distclean" script attempts to delete everything in the "src"
directory that is not part of the original distribution.

4. SYSTEM ADMINISTRATION FOR PROOFPOWER

4.A Setting the UNIX search path

An easy way to make the ProofPower binaries visible in the search path is to
add the ProofPower "bin" directory to the search path.  To do this add a line
into the file in your $HOME directory that is executed by the shell either when
you log in (e.g., .profile, .bash_profile, .login if you do a console log-in or
.xsession if you log-in via an X display manager) or when you start a shell
(e.g., .cshrc or .bashrc).  Consult your local documentation or your system
administrator if you need more information on your local configuration.

For example, if you use the Bourne shell or the Bourne Again shell, and the
ProofPower home directory is /usr/local/pp, then add the following line:

        PATH=/usr/local/pp/bin:$PATH

And if you use the C-shell, the equivalent line would be:

        setenv PATH /usr/local/pp/bin:$PATH

Some people prefer to extend the search path at the end rather than the
beginning, as in PATH=$PATH:/usr/local/pp/bin. But note that a printer
maintenance utility called "xpp" is installed on some Linux systems and would be
called in preference to the ProofPower program "xpp" if you put the ProofPower
bin directory at the end of the search path.

4.B Installing ProofPower in the standard bin directories.

If you wish to make the ProofPower software generally available on your
system, you can place symbolic links to the ProofPower executables
in one of the standard bin directories. For example, if you have installed
into /home/sw/pp2.7.6, you might do

        ln -s /home/sw/pp2.7.6/bin/* /usr/local/bin

It is advisable to follow the above example and make links to all the
executables. You must include a link to the findfile program because the shell
scripts use findfile to locate the ProofPower home directory.

4.C Uninstalling ProofPower

To uninstall ProofPower, delete the ProofPower home directory. This removes all
files created by the "install" script.  If you have created symbolic links to
the executables in one of the standard bin directories, the links will now be
broken and you will probably wish to  delete them.

4.D Copying the ProofPower Home Directory

If you need to copy the ProofPower home directory and you are using Poly/ML,
you need to use the poly command to change the absolute path name of the
parent of the example databases set up by the installation process
(example_hol.polydb and example_zed.polydb). Alternatively, you can delete
these databases and then rebuild them using the shell scripts install_holdemo
and install_zeddemo in the installation directory.
 
4.E Customising xpp

You can customise the xpp program by adding an X resource file in
$HOME/app-defaults/Xpp containing custom X resource settings.  Your starting
point for this is normally to take a copy of the files and links in the
"app-defaults" subdirectory of the ProofPower installation directory.  See the
xpp user guide (usr031) for more information.

4.F Summary of Environment Variables

See the configure script for details of environment variables that control the
build and installation of ProofPower.  There are also a number environment
variables that can be used to control the behaviour when a user runs ProofPower,
e.g., to control the TeX input search path used when running texdvi. These are
described below.

PPENVDEBUG - control diagnostics for the handling of the environment (tuning)

Default is no diagnostics. If set to a non-empty string the scripts and
xpp tell you what they are using for the various variables.

PPCOMPILER - ML compiler to use (SMLNJ or POLYML)

Default is planted in the scripts during installation, and selects whichever of
SML/NJ or Poly/ML was installed latest. Only relevant to developers who may
want to install with both compilers in one ProofPower home directory.

PPHOME - home directory for ProofPower

Default is calculated by a heuristic which determines the name of the
ProofPower home directory using the path name by which the script or program in
question was called and resolving symbolic links.

TEXINPUTS, BIBINPUTS, BSTINPUTS - for TeX, LaTeX and BibTeX

Default used in the scripts that run LaTeX and BibTeX is "$PPHOME/tex:". The
":" at the end means look in the standard places as well.  If you use other
programs such as xdvi that depend on TEXINPUTS, you may need to set this
environment variable to pick up some files (e.g., to see the PostScript
diagrams included in some of the documents).

PPDATABASEPATH - search path for databases

Default is ".:$HOME/db:$PPHOME/db".

N.b., if you want "." on PPDATABASEPATH, you need to put it there. It is
only tagged on automatically if you are defaulting this variable.

PPCOMPACT - control whether pp_make_database should do a compacting
garbage collection

Default "y".  Only relevant when PPCOMPILER is Poly/ML.  Set to "n" or
"N" to suppress compaction. Must be one of "y", "Y", "n" or "N".

PPETCPATH - search path used by the scripts to find the  sievekeyword and
sieveview files

The default is $PPHOME/etc.

5. KNOWN PROBLEMS

a) On some Linux installations, xpp command sessions may fail with the message

        xpp: system error: no pseudo-terminal devices available

This occurs if the Linux installation provides the grantpt interface for
accessing pseudo-terminals and does not support the older method that xpp
chooses by default on Linux.  Changing "#undef USE_GRANTPT" in the Linux
section of the file src/pterm.c to read "#define USE_GRANTPT" and reinstalling
xpp should fix this.

================================================================================
Special acknowledgments for contributions by Mark Adams of QinetiQ Ltd.

Rob Arthan. Lemma 1 Ltd. (See the ProofPower web-site for contact details).
================================================================================