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

14 Installation

At present, Twelf has been tested in SML of New Jersey (version 110 or higher), Poly/ML and MLton, all 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-4.tar.gz
tar -xf twelf-1-4.tar
cd twelf

This builds the Twelf server (see section 12 Twelf Server) for your current architecture and makes it accessible as `bin/twelf-server'. The make command is different for SML/NJ versions 110.20 or higher, for PolyML, and for MLton; see the list below. The make also installs the Twelf Emacs interface (see section 13 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.

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 13.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
See http://www.smlnj.org/ Because of minor incompatibilites between the officially released version 110.0.3 and newer versions (110.20 or higher) you have to compile Twelf for newer version of SML/NJ with with
make -f smlnj/Makefile
See http://www.polyml.org/ For Poly/ML you have to compile Twelf with
make -f polyml/Makefile
See http://www.mlton.org/ For MLton, you have to compile Twelf with
make -f mlton/Makefile

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