Twelf Copyright (C) 1997-1999, Frank Pfenning and Carsten Schuermann Authors: Frank Pfenning Carsten Schuermann With contributions by: Iliano Cervesato Jeff Polakow Twelf is an implementation of - the LF logical framework, including type reconstruction - the Elf constraint logic programming language - a meta-theorem prover for LF (very preliminary) - an Emacs interface This README file applies to version Twelf 1.2, internal revision R5. For current information regarding Twelf, see the Twelf home page at http://www.cs.cmu.edu/~twelf Twelf can be compiled and installed under Unix, either as a separate "Twelf Server" intended primarily as an inferior process to Emacs, or as a structure Twelf embedded in Standard ML. There is also self-extracting EXE file for Windows 95/98/NT for the Twelf server only. This is not described here---see Twelf home page for further information. Files ===== README --- this file Makefile --- enables make Makefile.NT --- enables make for NT load.sml --- enables use "load.sml"; (* especially for MLWorks *) make.sml --- used to build Twelf server bin/ --- utility scripts and heap location doc/ --- Twelf user's guide in various formats emacs/ --- Emacs interface for Twelf examples/ --- various case studies server.cm --- enables make of Twelf server sources.cm --- enables make of Twelf-SML src/ --- the SML sources for Twelf tex/ --- TeX macros and style files Installation Instructions ========================= These instructions apply to Unix or Windows 95/98/NT when compiling the sources directly. For Windows 95/98/NT there is also a self-extracting EXE file with a much simpler installation procedure, but for the Twelf Server only. Installation requires Standard ML, Revision of 1997. The Twelf Server requires SML of New Jersey. If it is not installed already, please check SML of New Jersey [free] http://cm.bell-labs.com/cm/cs/what/smlnj/index.html (version 110 or higher) MLWorks [commercial] http://www.harlequin.com/products/ads/ml/ml.html Platforms ========= Twelf can be installed on different platforms, such as Unix or Windows 95/98/NT. Note that these instructions are for SML of New Jersey, version 110 or higher. Twelf can be installed as Twelf-Server (a stand-alone version to be used primarily within Emacs) and Twelf-SML (a version embedded into SML) Instead of compiling Twelf for the Windows 95/98/NT family of operating systems, we recommend instead to use the precompiled version which is available from the Twelf homepage at http://www.cs.cmu.edu/~twelf/dist/twelf-1-2.exe Unix Installation ================= Summary ------- % gunzip twelf-1-2.tar.gz % tar -xf twelf-1-2.tar % cd twelf You may need to edit the file Makefile to give the proper location for sml-cm. These instructions are for SML of New Jersey, version 110 or higher. % make % bin/twelf-server Twelf 1.2, Aug 27 1998 %% OK %% You can now load the examples from the User's Guide and pose an example query as shown below. The prompt from the Twelf top-level is `?-'. To drop from the Twelf top-level to the ML top-level, type C-c (CTRL c). To exit the Twelf server you may issue the quit command or type C-d (CTRL d). Config.read examples/guide/sources.cfg Config.load top ?- of (lam [x] x) T. Solving... T = arrow T1 T1. More? y No more solutions ?- C-c interrupt %% OK %% quit % Detailed Instructions --------------------- Step 0: Select directory/Unpack Twelf distribution First select a directory where you want Twelf to reside. 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 install Twelf as root, a suitable directory would be /usr/local/lib but any other directory will work, too, as long it does not contain any whitespace characters. Since the distribution is unpacked into a subdirectory called `twelf' you should make sure such a directory does not already exist. Unpack the distribution in this directory: ( % is assumed to be the shell prompt.) % gunzip twelf-1-2.tar.gz % tar -xf twelf-1-2.tar % cd twelf Step 1: Compile Twelf You may need to edit the file Makefile to give the proper location for sml-cm (SML of New Jersey version 110 or higher, with the compilation manager pre-loaded). Twelf-Server: [Default] If you would like to build the Twelf server, whose primary use is as an inferior process to Emacs, call % make This builds the Twelf server for your current architecture and makes it accessible as bin/twelf-server. Under Linux, the heap image is about 1.6MB. It also installs the Twelf Emacs interface, but you must add a line (load "/emacs/twelf-init.el") into your .emacs file, where is the root directory into which you installed Twelf. To test whether the binary has been created properly, try % bin/twelf-server in the Twelf root directory. Use 'quit' to exit the server. Twelf-SML: If you would like to use Twelf as a structure in SML, you can then call % make twelf-sml in the root directory into which you installed Twelf. This creates bin/twelf-sml which is a rather large heap image (e.g., 11MB under Linux) since it include the SML/NJ compiler. Full installation: If you would like to install the Twelf-Server and Twelf-SML, you can then call % make all This builds both the Twelf-Server and Twelf-SML for your current architecture and makes them accessible as bin/twelf-server and bin/twelf-sml, respectively. It also installs the Twelf Emacs interface, but, as above, you must add a line (load "/emacs/twelf-init.el") into your .emacs file, where is the root directory into which you installed Twelf. Step 2: Removing temporary files The installation of the Twelf-Server and Twelf-SML creates various temporary files, which may be removed after a successful installation with % make clean Troubleshooting: Early versions of SML 110 of New Jersey do not support the switch for SML garbage collection messages from within SML triggered by the command SMLofNJ.Internals.GC.messages false; This feature is used in twelf-server.sml and twelf-sml.sml, the two files which compile the Twelf system. If SML complains about these lines either install a newer version of SML 110 of New Jersey, or comment out this line. Windows 95/98/NT Installation: ------------------------------ For the Windows 95/98/NT family of operating systems, we recommend the precompiled version of the Twelf server which is available from the Twelf homepage at http://www.cs.cmu.edu/~twelf/dist/twelf-1-2.exe which is a self-installing EXE file. NOTE: In order to run the provided examples, you must install Twelf into a directory without spaces in its name. If you want to instead compile Twelf for Windows 95/98/NT yourself, it is required that you also have gunzip.exe, tar.exe, make.exe and sed.exe on the path. These tools are publically available from ftp://microlib.cc.utexas.edu/microlib/nt/gnu/gnu-bin.tar.Z Twelf has been tested to work with NTEmacs which is freely available from the University of Washington: ftp://ftp.cs.washington.edu/pub/ntemacs Step 0: Select directory/Unpack Twelf distribution First select a directory where you want Twelf to reside. 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 install Twelf as root, a suitable directory would be C:\ but any other directory will work, too, as long as it does not contain any whitespace characters. Since the distribution is unpacked into a subdirectory called `twelf' you should make sure such a directory does not already exist. Unpack the distribution in this directory C:> gunzip twelf.tar.gz C:> tar -xvf twelf.tar then C:> cd twelf You must then edit the file Makefile.NT to give the proper location for sml-cm, and the root directory into which you unpacked Twelf (in our example set the variable "twelfdir" to C:\twelf). Step 1: Compile Twelf Twelf-Server: [Default] If you would like to build the Twelf server, whose primary use is as an inferior process to Emacs, call C:> make -f Makefile.NT This builds the Twelf server for your current architecture and makes it accessible as bin\twelf-server.bat. It also installs the Twelf Emacs interface, but you must add a line (load "/emacs/twelf-init.el") into your C:\_emacs file, where is the root directory into which you installed Twelf, using slashes instead of backslashes for the path. To test whether the binary has been created properly, try C:> bin\twelf-server in the Twelf root directory. Twelf-SML: If you would like to use Twelf as a structure in SML, you can then call C:> make twelf-sml -f Makefile.NT in the root directory into which you installed Twelf. This creates bin\twelf-sml.bat. Full installation: If you would like to install the Twelf-Server and Twelf-SML, you can then call C:> make all -f Makefile.NT This builds both the Twelf-Server and Twelf-SML for your current architecture and makes them accessible as bin\twelf-server.bat and bin\twelf-sml, respectively. It also installs the Twelf Emacs interface, but, as above, you must add a line (load "/emacs/twelf-init.el") into your C:\_emacs file, where is the root directory into which you installed Twelf, using slashes instead of backslashes for the path. Step 2: Removing temporary files The installation of the Twelf-Server and Twelf-SML creates various temporary files, which may be removed after a successful installation with C:> make clean -f Makefile.NT