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.  
------------------------------------------------------------------------------