F.2 INSTALL
------------------------------------------------------------------------------
INSTALL
Installation notes for the RISC ProgramExplorer.
Author: Wolfgang Schreiner <Wolfgang.Schreiner@risc.jku.at>
Copyright (C) 2008-, 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 3 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, see <http://www.gnu.org/licenses/>.
------------------------------------------------------------------------------
Installing the RISC ProgramExplorer
-----------------------------------
The RISC ProgramExplorer 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 ProgramExplorer 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 ProgramExplorer, 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 A-C are described below,
but please read the following remark first.
Mathematical Fonts in the RISC ProgramExplorer
----------------------------------------------
After an installation of the RISC ProgramExplorer, the mathematical fonts
displayed by the RISC ProgramExplorer (i.e. by the embedded Mozilla browser) may
not look nice. For an aesthetically pleasing display, proceed as described on
Fonts for MathML-enabled Mozilla
https://developer.mozilla.org/en/Mozilla_MathML_Project/Fonts
In a nutshell, create in your home directory a subdirectory ~.fonts~,
download into this directory the STIX font archive ~STIX-mozilla1.9.zip~,
and unzip the archive (which will create a number of font files .fonts/*.otf~).
Then (re)start the RISC ProgramExplorer.
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 6.0 ~squeeze~ 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 7 or higher runtime environment.
You can download a JRE 7 from
http://www.oracle.com/technetwork/java/javase/downloads/index.html
2) The Mozilla Firefox or SeaMonkey browser.
On a Debian 7.0 GNU/Linux system, just install the package
~xulrunner-10.0~ by executing (as superuser) the command
apt-get install xulrunner-10.0
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 or Solaris?~ The RISC ProgramExplorer 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 6.0 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 RISC ProgramExplorer, first create a directory INSTALLDIR
(where INSTALLDIR can by any directory path). Download from the website the
file
ProgramExplorer-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 ProgramExplorer-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/
ProgramExplorer ... the main script to start the program
cvcl ... CVC Lite, a validity checker used by the software.
doc/
index.html ... API documentation
examples-ProgramExplorer-CVC3/
README ... short explanation of examples
*.theory ... some example theories
*.java ... some example program specifications
PETASKS.tgz ... an archive of sample program verifications
examples-ProofNavigator-CVC3/
README ... short explanation of examples
*.pn ... examples of RISC ProofNavigator theories
lib/
Screenshot.png ... startup splash screen
*.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~
ProgramExplorer/
Main.java ... the main class for the RISC ProgramExplorer
ProofNavigator/
*.java ... the sources for the RISC ProofNavigator
External/
*.java ... third-party sources
Open in a text editor the script ~ProgramExplorer~ 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
ProgramExplorer
to run the RISC ProgramExplorer. If you rename/copy/link the script to
~ProofNavigator~ and execute
ProofNavigator
the program starts with a standalone interface to the RISC ProofNavigator.
B) Compiling the Source Code
----------------------------
To compile the Java source, first make sure that you have the Java 7 SE
development environment installed. You can download the Java 7 SE from
http://www.oracle.com/technetwork/java/javase/downloads/index.html
Furthermore, on a GNU/Linux system you need also the Mozilla Firefox or
SeaMonkey browser, GTK2 and the GIMP toolkit GTK+ installed (see Section A).
Now download the distribution and unpack it as described in Section A.
The RISC ProgramExplorer 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/*:../lib/swt32/*~ fmrisc/ProgramExplorer/Main.java
(replace ~swt32~ by ~swt64~ on a 64bit system).
You may 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 fmrisc/*/*/*/*.class
Finally, you have to customize the ~ProgramExplorer~ 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://en.wikipedia.org/wiki/Comparison_of_Subversion_clients for a list of
available clients. On a computer with the Debian 6.0 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.jku.at/schreine/FM-RISC/tags/VERSION
If you have the ~svn~ command-line client installed, execute the command
svn export
svn://svn.risc.jku.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.
------------------------------------------------------------------------------