CLaReT: The Computer Language Reasoning Tool

Copyright 1994, 1995, 1996 by University of Cambridge.
Copyright 1997, 1998, 1999 by University of Edinburgh.

See the COPYRIGHT file for details.

Distribution

CLaReT is available by anonymous ftp from ftp.cl.cam.ac.uk in the directory hvg/claret/ or on the World Wide Web at http://www.cl.cam.ac.uk/ftp/hvg/claret/. The distribution unpacks to a number of files and subdirectories including the following:

COPYRIGHT Copyright notice, license and disclaimer
Makefile A file for automatically building the system
READ-ME.html This file
Version The version number
doc/ Manuals
examples/ Directory of examples
nested_rec_def_type.patch Patch for pre-HOL90.10 versions of the nested_rec library
runtime/ Support code required by files generated using CLaReT
sml/ A directory containing various subsystems
syn_tree/ Syntactic support for concrete representations of trees

Installation

To build CLaReT you will first need to install Standard ML of New Jersey version 110 or later, including sources for ML-Lex and ML-Yacc. Let smlnj denote the full path to your installation of Standard ML of New Jersey (the root of the source directory, not a path to the executable). To build CLaReT, move into the unpacked distribution directory and type: 
   make SMLNJ_SRC=smlnj
After the build has completed successfully, a shell script to run SML/NJ with a CLaReT heap for your architecture will be found in bin/claret. To build CLaReT for other architectures simply run make again on a suitable machine. Rather than specifying the path to SML/NJ on the command line every time, you may wish to edit the Makefile.

Further Information

For further information visit the CLaReT web page at: http://www.cl.cam.ac.uk/Research/HVG/claret/.