Go to the first, previous, next, last section, table of contents.


13 Installation

At present, Twelf has been tested in SML of New Jersey (version 110 or higher) and MLWorks, both of which implement Standard ML (revised 1997) and the Standard ML Basis Library. The instructions below apply to a Unix system. For instructions for other architectures or updates please check the file `INSTALL' at the Twelf home page and in the Twelf root directory after unpacking the distribution.

On a Unix system you unpack the sources with

gunzip twelf-1-3.tar.gz
tar -xf twelf-1-3.tar
cd twelf
make

This builds the Twelf server (see section 11 Twelf Server) for your current architecture and makes it accessible as `bin/twelf-server'. It also installs the Twelf Emacs interface (see section 12 Emacs Interface), but you must add a line

(load "directory/emacs/twelf-init.el")

to your `.emacs' file, where directory is the root directory into which you installed Twelf. Note that the Twelf installation cannot be moved after it has been compiled with make, since absolute pathnames are built into the executable scripts.

Note that the Twelf server presently only works with Standard ML of New Jersey, since interrupt handling is implementation specific.

If you would like to use Twelf as a structure in SML, you can then call

make twelf-sml

which creates `bin/twelf-sml' for the Twelf-SML mode (see section 12.11 Twelf-SML Mode). Calling make clean will remove temporary files created by the SML compiler, but not the executable file.

SML of New Jersey (free, version 110 or higher)
See http://cm.bell-labs.com/cm/cs/what/smlnj/index.html
MLWorks (commercial)
See http://www.harlequin.com/products/ads/ml/ml.html In MLWorks, you can presently only directly load the Twelf sources, using the file `load.sml'.
mlworks-basis  start MLWorks with basis library in Twelf root directory
use "load.sml";  compile and load Twelf


Go to the first, previous, next, last section, table of contents.