C.2 INSTALL
------------------------------------------------------------------------------
INSTALL
Installation notes for 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
------------------------------------------------------------------------------
Installation
------------
The RISC ProofNavigator is available for computers with x86-compatible
processors (32 bit as well as 64 bit) running under the GNU/Linux operating
system. The core of the RISC ProofNavigator is written in Java but it depends
on various third-party open source libraries and programs that are
acknowledged in the README file.
To use the RISC ProofNavigator, you have three options:
A) You can just use the distribution, or
B) you can compile the source code contained in the distribution, or
C) you can download the source from a Subversion repository and compile it.
The procedures for the three options are described below.
A Note for Microsoft Windows Users
----------------------------------
The RISC ProofNavigator does currently not run natively under MS Windows.
However, you can find on the RISC ProofNavigator web page a link to a virtual
machine with a Debian 4.0 GNU/Linux distribution that includes an installation
of the RISC ProofNavigator. The virtual machine is in the format of the free
virtualization environment VirtualBox (http://www.virtualbox.org). Install on
your MS Windows PC the VirtualBox software and the virtual machine (see the
web page for further instructions) and you can enjoy the RISC ProofNavigator
also under MS Windows.
A) Using the Distribution
-------------------------
We provide a distribution for computers with ix86-compatible processors
running under the GNU/Linux operating system (the software has been developed
on the Debian 3.1 "sarge" distribution, but any other distribution will work
as well). If you have such a computer, you need to make sure that you also
have
1) A Java 5 or higher runtime environment.
You can download the Sun JRE 5.0 from
http://java.sun.com/j2se/1.5.0/download.jsp
2) The Mozilla Firefox or SeaMonkey browser.
On a Debian 4.0 GNU/Linux system, just install the package
"iceweasel" by executing (as superuser) the command
apt-get install iceweasel
On other Linux distributions, first look up the FAQ on
http://www.eclipse.org/swt/faq.php
for the question "What do I need to run the SWT browser in a standalone
application on Linux GTK or Linux Motif?" The ProofNavigator uses the
SWT browser, thus you have to install the software described in the FAQ.
See the README file for further information.
3) The GIMP Toolkit GTK+ 2.6.X or higher.
On a Debian 3.1 GNU/Linux system, GTK+ is automatically installed,
if you install the Mozilla browser as described in the previous paragraph.
On other Linux distributions, download GTK+ from http://www.gtk.org
For installing the ProofNavigator, first create a directory INSTALLDIR (where
INSTALLDIR can by any directory path). Download from the website the file
ProofNavigator-VERSION.tgz
(where VERSION is the number of the latest version of the ProofNavigator) into
INSTALLDIR, go to INSTALLDIR and unpack by executing the following command:
tar zxf ProofNavigator-VERSION.tgz
This will create the following files
README ... the readme file
INSTALL ... the installation notes (this file)
CHANGES ... the change history
COPYING ... the GNU Public License
bin/
ProofNavigator ... the main script to start the program
cvcl ... CVC Lite, a validity checker used by the software.
doc/
index.html ... API documentation
examples/
README ... short explanation of examples
*.pn ... some example specifications and proofs
lib/
*.jar ... Java archives with the program classes
swt32/ ... SWT for GNU/Linux computers with 32 bit processors
swt.jar
*.so
swt64/ ... SWT for GNU/Linux computers with 64 bit processors
swt.jar
*.so
manual/
main.pdf ... the PDF file for the manual
index.html ... the root of the HTML version of the manual
src/
fmrisc/ ... the root directory of the Java package "fmrisc"
ProofNavigator/
Main.java ... the main class for the ProofNavigator
Open in a text editor the script "ProofNavigator" in directory "bin" and
customize the variables defined for several locations of your environment. In
particular, the distribution is configured to run on a 32-bit processor. If
you use a 64-bit processor, uncomment the line "SWTDIR=$LIBDIR/swt64" (and
remove the line "SWTDIR=$LIBDIR/swt32").
Put the "bin" directory into your PATH
export PATH=$PATH:INSTALLDIR/bin
You should now be able to execute
ProofNavigator
If you happen to get a message that ends with
...
ERROR: You may try "ProofNavigator --nogui".
your Mozilla installation could not be detected. In this case, please set the
value of the variable MOZILLA_FIVE_HOME in the "ProofNavigator" script to the
location of the Mozilla libraries (e.g. /usr/lib/mozilla). In any case, you
should be able to start
ProofNavigator --nogui
to get a text-only interface.
B) Compiling the Source Code
----------------------------
To compile the Java source, first make sure that you have the Java 5
development environment installed. You can download the Sun JDK 5.0 from
http://java.sun.com/j2se/1.5.0/download.jsp
Furthermore, on a GNU/Linux system you need also the Mozilla browser 1.7.X
GTK2 and the GIMP toolkit GTK+ 2.X installed (see Section A).
Now download the distribution and unpack it as described in Section A above.
The ProofNavigator distribution contains an executable of the validity
checker CVC Lite for GNU/Linux computers with x86-compatible processors. To
compile the validity checker for other systems, you need to download the
CVC Lite source code (see the README file) and compile it with a C++
compiler. See the CVC Lite documentation for more details.
To compile the Java source code, go to the "src" directory and execute from
there
javac -cp ".:../lib/antlr.jar:../lib/om-lib.jar:../lib/swt.jar"
fmrisc/ProofNavigator/Main.java
(ignore the warning about "unchecked" or "unsafe" operations, this refers to
Java files generated automatically from ANTLR grammars).
Then execute
jar cf ../lib/fmrisc.jar fmrisc/*/*.class fmrisc/*/*/*.class
Finally, you have to customize the "ProofNavigator" script in directory "bin"
as described in Section A. You should then be able to start the program by
executing the script.
C) Downloading the Source Code from the Subversion Repository
-------------------------------------------------------------
You can now download the source code of any version of the ProofNavigator
directly from the ProofNavigator Subversion repository.
To prepare the download, first create a directory SOURCEDIR (where SOURCEDIR
can be any directory path).
To download the source code, you need a Subversion client, see
http://subversion.tigris.org/project_links.html for a list of available
clients. On a computer with the Debian 3.1 distribution of GNU/Linux, it
suffices to install the "svn" package by executing (as superuser) the command
apt-get install svn
which will provide the "svn" command line client.
Every ProofNavigator distribution has a version number VERSION (e.g. "0.1"),
the corresponding Subversion URL is
svn://svn.risc.uni-linz.ac.at/schreine/FM-RISC/tags/VERSION
If you have the "svn" command-line client installed, execute the command
svn export
svn://svn.risc.uni-linz.ac.at/schreine/FM-RISC/tags/VERSION SOURCEDIR
to download the source code into SOURCEDIR. With other Subversion clients, you
have to check the corresponding documentation on how to download a directory
tree using the URL svn://... shown above.
After the download, SOURCEDIR will contain the files of the distribution as
shown in Section A; you can compile the source code as explained in Section B.
------------------------------------------------------------------------------
End of INSTALL.
------------------------------------------------------------------------------
Wolfgang
Schreiner
