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