Getting and compiling Twelf

Getting the sources:

The very newest versions are from CVS. Some previous versions are on the webpage, but really, I recommend the CVS version.
cvs -d :pserver:guest_lf@cvs.concert.cs.cmu.edu:/cvsroot checkout twelf
This will create a new directory named twelf in the current directory, with sources and a bunch of examples.

Building it:

There's two options: SML/NJ, and Poly/ML. The SML/NJ option is more heavily used, in CMU and Princeton at least.

With a recentish version of SML/NJ (110.20 or greater), from the twelf top-level directory, type
make -f smlnj/Makefile

With an older version (110.0.7 for example), just
make
would work

If you have Poly/ML in your path, the following should also work:
make -f polyml/Makefile

Running it:

A binary named twelf-server will appear in the bin subdirectory. It can be run on its own, or as a subprocess under emacs, which allows various key bindings (if you add the appropriate lines to your emacs configuration). A separate target called twelf-sml also creates a SML structure named Twelf, which can be invoked by SML programs.

Examples:

A bunch of examples are in the examples subdirectory.

Manual:

The manual.