------------------------------------------------------------------------------ INSTALL Installation notes for the RISC ProofNavigator. Author: Wolfgang Schreiner Copyright (C) 2005-, Research Institute for Symbolic Computation (RISC) Johannes Kepler University, Linz, Austria, http://www.risc.jku.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 5.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 6 or higher runtime environment. You can download the Sun JRE 6 from http://java.sun.com/j2se 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 swt64/ ... SWT for GNU/Linux computers with 64 bit processors swt.jar 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 or higher 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. ------------------------------------------------------------------------------