Download
From The Twelf Project
Follow the instructions below to download and install Twelf. You can also try Twelf live in your browser.
Contents |
Getting Twelf
Currently, the two recommended versions of Twelf are the (semi-stable) CVS version and the 1.5R1 version. The CVS version can be obtained from anonymous CVS or from the nightly build process; both of these are described below.
Twelf Night(ly)
The Twelf Night(ly) system checks the CVS tree nightly; if changes have been made to Twelf, it creates a new source distribution, as well as a binary distribution for Linux complied with the fast MLton complier. The website also includes a relatively recent Windows installer for Twelf.
Before you download the, check the log messages and make sure nothing seems out of the ordinary. If anything seems wrong, or if the Windows binary is out of date, contact Rob who maintains the system.
Twelf CVS
CVS comes installed on most Linux systems and Mac OS X systems, and can be obtained from nongnu.org for other operating systems, including Windows. If CVS is installed, the CVS version of Twelf can be anonymously checked out by executing the following commands at a command line:
cvs -d :pserver:guest_lf@cvs.concert.cs.cmu.edu:/cvsroot login cvs -d :pserver:guest_lf@cvs.concert.cs.cmu.edu:/cvsroot checkout twelf
These commands will download all of the Twelf source code into a directory called "twelf" inside of the directory you are in when you execute the commands.
Twelf 1.5R1 (March 1, 2005)
The most recent release of Twelf, 1.5R1, can be downloaded from the CMU Twelf website, though the development version (above) has certain features, such as %trustme, that are not available in this release.
twelf-1-5R1.tar.gz (1157430 bytes, md5: 05b5c65f297c1f4ee07641682121ebbc)
- Requires a pre-existing ML installation (see the installation instructions below for more information)
- Supports SML/NJ 110.0.07, SML/NJ 110.53, Poly/ML 4.1.3 and MLton 20040227
On Unix-like systems, the following command will unpack the source code into a new folder called "twelf" inside of the directory where you run the command:
tar -xzvf twef-1-5R1.tar.gz
Older versions of Twelf
Links to older software versions are available from the revision history page, but use of any version earlier than 1.5R1, especially when working with metatheorems, is highly discouraged.
Installation instructions
Pre-compiled versions
If you download the pre-compiled Linux or Windows versions of Twelf, simply run the installer (on Windows) or unpack the tarball wherever you want to put the distribution (on Linux), and the skip to the instructions for setting up Emacs below.
Installing with SML/NJ
You will need to have the Standard ML of New Jersey software on your computer. This can be obtained from the SML/NJ website. Additionally, you will need the standard unix-style Make tools. These come with basically any Linux distribution. Windows users should check out the Cygwin Project to install those tools under Windows. Once you have these things set up, Twelf can be built by running the following commands:
$ cd twelf $ make -f smlnj/Makefile
Installing with MLton
You will need to have the MLton compiler installed on your system. This can be obtained from the MLton website. Using Twelf with MLton has not been tested on Windows. On Linux, Twelf can be built by running the following commands:
$ cd twelf $ make -f mlton/Makefile
Setting up Emacs
A piece of information about using Twelf with Emacs is printed out by the installation script, telling you to add two lines somewhere in your .emacs file. If you don't have a .emacs file in your home directory, you can create one and add these two lines.
If you put Twelf in the directory /somewhere/twelf/ then you should add these lines (just replace somewhere with wherever you built Twelf).
(setq twelf-root "/somewhere/twelf/") (load (concat twelf-root "emacs/twelf-init.el"))
When using the Windows installer, the default directory is C:\Program Files\Twelf, so
(setq twelf-root "C:\Program Files\Twelf") (load (concat twelf-root "emacs\twelf-init.el"))
