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

This builds the Twelf server (see section 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 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 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/

<UL> <LI> <A HREF="http://www.smlnj.org/">SML of New Jersey Home Page</A> </LI> </UL>

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

Poly/ML

See http://www.polyml.org/

<UL> <LI> <A HREF="http://www.polyml.org/">Poly/ML Home Page</A> </LI> </UL>

For Poly/ML you have to compile Twelf with

make -f polyml/Makefile

MLton

See http://www.mlton.org/

<UL> <LI> <A HREF="http://www.mlton.org/">MLton Home Page</A> </LI> </UL>

For MLton, you have to compile Twelf with

make -f mlton/Makefile

This document was generated by Florian Rabe on April, 3 2009 using texi2html 1.76.