Twelf with Emacs

From The Twelf Project
Jump to: navigation, search

The preferred way to interact with Twelf is through its emacs mode, which is included in the Twelf distribution. The Download page has basic information for setting up Emacs mode with Twelf.

Prerequisites

These instructions assume you've already downloaded Twelf, and that either

  • You used the Windows/OSX installer
  • You downloaded a pre-compiled tarball
  • You downloaded a source tarball and have already built Twelf

These instructions should easily translate to using Subversion to get Twelf, however.

Installing the Twelf emacs mode

Add the following to your Emacs configuration file, which should be the file .emacs in your home directory.

(setq twelf-root "/somewhere/twelf/") (load (concat twelf-root "emacs/twelf-init.el"))

For instance, if the directory where you unpacked the tarball is /usr/local/twelf, then you'll want those two lines to be:

(setq twelf-root "/usr/local/twelf/") (load (concat twelf-root "emacs/twelf-init.el"))

If your Twelf directory is /home/foo/stuff/logic/twelf, then you'll want those lines to be:

(setq twelf-root "/home/foo/stuff/logic/twelf/") (load (concat twelf-root "emacs/twelf-init.el"))

If you used the default Windows installer, you'll want those to lines to be

(setq twelf-root "C:\\Program Files\\Twelf\\") (load (concat twelf-root "emacs\\twelf-init.el"))

Exit Emacs and restart it.

How Twelf programs are divided up into files

  1. Twelf programs should be stored in files with the .elf extension.
  2. All of the .elf files in a project are collected in a configuration file, typically called sources.cfg. A configuration file lists (paths to) individual .elf files in dependency order. You can load a configuration file, which loads each .elf file in sequence.

Creating a .cfg file

Start Emacs in some directory (for the purposes of this description, we'll assume it's ~/tmp/twelf. Create the configuration file sources.cfg with the following text in it:

sometwelf.elf

Save the file (by using CTRL-x CTRL-s in Emacs).

Creating a .elf file

Then create a file sometwelf.elf (by using CTRL-x CTRL-f in Emacs) and enter the following text:

nat : type.
z : nat.
s : nat -> nat.
ss : nat -> nat = [n] s (s n).

plus : nat -> nat -> nat -> type.
plus/z : plus z N N.
plus/s : plus N M P -> plus (s N) M (s P).

Save the file (by using CTRL-x CTRL-s in Emacs).

Using the Twelf emacs mode

You use Twelf by asking it to process declarations. Twelf responds by either printing Server OK at the bottom of the screen if your declarations were processed successfully, or by popping up the twelf-server buffer if there was an error (ABORT).

The emacs mode allows you to process declarations at a variety of granularities:

  • A whole configuration file (CTRL-c CTRL-c loads a cfg file)
  • A whole .elf file (CTRL-c CTRL-s loads the .elf file open in the current emacs window)
  • A single declaration (thing ending in a period) (CTRL-c CTRL-d loads declaration the cursor is on in the in the current .elf file)

For example, a typical use case is to load your entire project with CTRL-c CTRL-c when you start working, and then to process new Twelf code declaration-by-declaration as you write it, using CTRL-c CTRL-d. Sometimes you will go back and make edits in lots of different places in a file, in which case it's helpful to reload just the current file with CTRL-c CTRL-s.

Only reloading the configuration clears the state of Twelf. Even reloading will not clear previous declarations from the file (though it will typically shadow them). This might give unexpected results if you remove a declaration and expect it to have disappeared.

Loading the configuration file: CTRL-c CTRL-c

Assuming you still have sometwelf.elf open in emacs, hit CTRL-c CTRL-c. If sometwelf.elf has unsaved changes, you will be asked:

File not in current configuration. Save? (yes or no)

Type yes.

You will then be asked:

Visit config file: (default sources.cfg) ~/tmp/twelf/

This is asking for the location of the sources.cfg file you saved when following the instructions above; the default option is the correct one. Just hit ENTER.

You will then be asked:

Twelf server: (default twelf-server) /something/bin/ This is asking which Twelf binary you want to run; the default should already be correct, just hit ENTER.

This will process your configuration file, which in turn says to process sometwelf.elf.

Checking an individual declaration: CTRL-c CTRL-d

Now you can type new declarations into the emacs buffer and use CTRL-c CTRL-d to load them.

Checking an individual file: CTRL-c CTRL-s

Or you can reload the file in the current window with CTRL-c CTRL-s. You must previously have loaded a configuration file.

Syntax highlighting

Twelf does not automatically refresh its syntax highlighting as you type. You can manually refresh the highlighting as follows:

  1. CTRL-c l fontifies the currently visible emacs buffer. E.g. in sometwelf.elfm the constants (nat, plus/z, etc.) should turn red, the bound variable n should turn green, and the logic-programming variables N, M, and P should turn blue.
  2. CTRL-c CTRL-l fontifies the current declaration only. This is useful if you have really big files.

For more info on the emacs mode, see Emacs Interface in the User's Guide.

Hacks

If you use multiple frames with Emacs, twelf-mode annoyingly pops up the Twelf server buffer in the current frame, even if it is already shown in another frame. To avoid this, set display-buffer-reuse-frames to t. Now, you will still have the problem that although the buffer is shown, it does not scroll to the bottom; to fix this you need to edit twelf.el and change (get-buffer-window twelf-server-buffer) to (get-buffer-window twelf-server-buffer t).

See also