C.2 INSTALLC System InstallationC.1 README

C.1 README

------------------------------------------------------------------------------
README
Information on the RISC ProofNavigator.

Author: Wolfgang Schreiner <Wolfgang.Schreiner@risc.uni-linz.ac.at>
Copyright (C) 2005-, Research Institute for Symbolic Computation (RISC)
Johannes Kepler University, Linz, Austria, http://www.risc.uni-linz.ac.at

This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA
------------------------------------------------------------------------------

RISC ProofNavigator
-------------------
http://www.risc.uni-linz.ac.at/research/formal/software/ProofNavigator

This is the RISC ProofNavigator, an interactive proof assistant for supporting
formal reasoning about computer programs and computing systems. This software
is freely available under the terms of the GNU General Public License, see
file COPYING.

The RISC ProofNavigator runs on computers with x86-compatible processors
running under the GNU/Linux operating system. For installation instructions,
see file INSTALL. For learning how to use the software, see the file
"main.pdf" in directory "manual"; several proof examples can be found in
directory "examples".

Please send bug reports to the author of this software:

  Wolfgang Schreiner <Wolfgang.Schreiner@risc.uni-linz.ac.at>
  http://www.risc.uni-linz.ac.at/people/schreine
  Research Institute for Symbolic Computation (RISC)
  Johannes Kepler University
  A-4040 Linz, Austria

Third Party Software
--------------------
The ProofNavigator uses the following open source programs and libraries. Most
of this is already included in the ProofNavigator distribution, but if you
want or need, you can download the source code from the denoted locations
(local copies are available on the ProofNavigator web site) and compile it on
your own.  Many thanks to the respective developers for making this great
software freely available!

CVC Lite 2.0
http://www.cs.nyu.edu/acsys/cvcl
-------------------------------
This is a C++ library/program for validity checking in various theories.

The ProofNavigator currently only works with CVCL 2.0, not any of the later
CVCL versions available from the CVCL web site. To download the CVCL 2.0
source, go to the RISC ProofNavigator web site (URL see above), Section "Third
Party Software", and click on the link "CVCL 2.0 local copy".

RIACA OpenMath Library 2.0
http://www.riaca.win.tue.nl/products/openmath/lib
-------------------------------------------------
This is a library for converting mathematical objects to/from 
the OpenMath representation.

Go to the link "OMLib 2.0" and then "Downloads".
Download one of the "om-lib-src-2.0-rc2.*" files.

General Purpose Hash Function Algorithms Library
http://www.partow.net/programming/hashfunctions
-----------------------------------------------
A library of hash functions implemented in various languages.

Go to the link "General Hash Function Source Code (Java)" to download
the corresponding zip file.

ANTLR 2.7.6b2
http://www.antlr.org
--------------------
This is a framework for constructing parsers and lexical analyzers.

On a Debian 3.1 GNU/Linux distribution, just install the package "antlr"
by executing (as superuser) the command

  apt-get install antlr

The Eclipse Standard Widget Toolkit 3.3
http://www.eclipse.org/swt
---------------------------------------
This is a widget set for developing GUIs in Java.

Go to section "Stable" and download the version "Linux (x86/GTK2)" (if you use
a 32bit x86 processor) or "Linux (x86_64/GTK 2)" (if you use a 64bit x86
processor).

Mozilla Firefox 2.0.X or SeaMonkey  1.1.X (or higher)
http://www.mozilla.org
-----------------------------------------------------
See the question "What do I need to run the SWT browser in a standalone
application on Linux GTK or Linux Motif?" in the FAQ at
http://www.eclipse.org/swt/faq.php.

Chances are that the SWT browser will work with the Firefox included in your
Linux distribution (but it will *not* work with the Firefox downloaded from
the Mozilla site). For instance, on a Debian 4.0 GNU/Linux distribution, just
install Firefox by executing (as superuser) the command

  apt-get install iceweasel

If the SWT browser does not work with the Firefox included in your GNU/Linux
distribution, go to the page http://www.mozilla.org/projects/seamonkey to
download and install the SeaMonkey 1.1.4 browser instead. You might have to
set the environment variable MOZILLA_FIVE_HOME in the "ProofNavigator" script
to "/usr/lib/mozilla".

The GIMP Toolkit GTK+ 2.X (or higher)
http://www.gtk.org
-------------------------------------
This library is required by "Eclipse Linux (x86/GTK2)" and by 
"Mozilla 1.7.8 GTK2".

On a Debian 3.1 GNU/Linux distribution, the package is automatically
installed, if you install the "mozilla-browser" package (see above).

On another GNU/Linux distribution, go to the GTK web package, section
"Download", to download GTK+.

Java Development Kit 5.0 (or higher)
http://java.sun.com/j2se/1.5.0
------------------------------------
Go to the "Downloads" section to download the Sun JDK 5.0. The ProofNavigator
does currently not use any of the Java 5 language features and can therefore
be also compiled with JDK 1.4.2 (but this may change in the future).

Tango Icon Library 0.6.1
http://tango-project.org/
-------------------------
Go to the "Base Icon Library" section, subsection "Download", to download
the icons used in the ProofNavigator.

------------------------------------------------------------------------------
End of README.
------------------------------------------------------------------------------


Wolfgang Schreiner

C.2 INSTALLC System InstallationC.1 README