This file describes the installation 
of the CCSL compiler version 2.2.6.

######################################################################
# $Id: INSTALL.in,v 1.3 2003/08/21 16:38:30 tews Exp $
######################################################################


SYSTEM REQUIREMENTS

The CCSL compiler should run on any platform that is supported by
ocaml. That is, on any POSIX-compliant system as well as on MS
Windows and on the Macintosh, see
http://caml.inria.fr/ocaml/portability.html for details. I have
tested it on Linux (Debian and RedHat) and on SunOS 5.6. If you
compile it on any other platform, please drop me a note. 


PREREQUISITES

you need:
   - GNU make, available at http://www.gnu.org/software/make/
   - ocaml, available at http://caml.inria.fr/ocaml/
     (ocaml version 3.x is sufficient)
   - either PVS or Isabelle/HOL,
	PVS is available at http://pvs.csl.sri.com/
	Isabelle is available at http://isabelle.in.tum.de/

   Strictly speaking neither PVS nor Isabelle/HOL are necessary
   to run the CCSL compiler. But the compiler will be pretty much
   useless without one of the theorem provers.


INSTALLATION INSTRUCTIONS

1. untar the sources

   zcat ccsl-2.2.6.tar.gz | tar -xf -

   or

   tar -xzf ccsl-2.2.6.tar.gz

2. configure the sources, start

   cd ccsl-2.2.6
   ./configure

   This checks for ocaml and sets the installation directory. 
   The "configure" script accepts the following parameters:

   --bindir=DIR                           (default /usr/local/bin)
	sets the directory where the compiler will be installed.

   --elibdir=DIR                   (default /usr/local/share/emacs/site-lisp)
	sets the directory for the emacs lisp files for the CCSL Emacs mode

   --mandir=DIR                           (default /usr/local/man)
	directory for the man page

   --prefix=PREFIX                        (default /usr/local)
	Set the prefix for --bindir, and --mandir.
	--prefix=DIR is equivalent to
	--bindir=DIR/bin --mandir=DIR/man \
	--elibdir=DIR/share/emacs/site-lisp

   --ocamlbindir=DIR                      (default empty)
	Use this option only if ocamlc is not found in your path, 
	or if the ocaml found in the path is not the right one.

   --help
	prints usage information

   
   In case the "configure" script fails:
    - edit the top section of ccsl-2.2.6/Makefile. 
    - copy Doc/ccslc.1.in to Doc/ccslc.1 and substitute the PVS
      library directory for the string "@mllibdir@".
   
   [
    Why is configuration neccessary?

    Configuration is not really necessary. It used to be back 
    in those days when CCSL used an external PVS library. 
    Configuration will speed up configuration if you have ocamlc.opt 
    available.
   ]

4. compile

   make all

   This creates the CCSL compiler ccslc in subdirectory Ccsl. 
   Run it like
   
     Ccsl/ccslc your-specification.beh

5. (optional) If your system supports the ocaml native
   code compiler you can built the optimised CCSL compiler
   ccslc.opt via

   make opt


6. Install

   make install


   Installation creates the following files:

   in directory BINDIR

      ccslc
      ccslc.opt

   in directory ELIBDIR

      ccsl-mode.el
      loop-compile.el


7. (recommended for emacs users) configure the ccsl emacs mode:

  Add the following lines to your ~/.emacs. Substitute the correct 
  location of the emacs lisp files if you changed the default location
  /usr/local/share/emacs/site-lisp.

  ;; Extend `load-path' 
  (setq load-path
    (cons "/usr/local/share/emacs/site-lisp" load-path))

  ;; Setup autoloading the `ccsl-mode'.
  (setq auto-mode-alist
    (cons '("\\.beh\\'" . ccsl-mode) auto-mode-alist))

  (autoload 'ccsl-mode "ccsl-mode"
    "Major mode for editing ccsl." t nil)