Documentation out of dateLearn more

Twelf with Emacs

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

Prerequisites

These instructions assume you’ve already downloaded STELF, and that either

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

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

Installing the STELF emacs mode

If you put STELF in the directory /somewhere/twelf/ then you should have these two lines (just replace somewhere with wherever you put your STELF):

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 STELF 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\\STELF\\")
(load (concat twelf-root "emacs\\twelf-init.el"))

Exit Emacs and restart it.

How STELF programs are divided up into files

STELF programs should be stored in files with the .elf extension.
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:

%sort nat %.
%term z nat %.
%term s %pi nat %-> nat %.
%define ss (%pi nat %-> nat) [n] s (s n) %.
%sort plus {_ nat} {_ nat} {_ nat} %.
%term plus/z plus z N N %.
%term plus/s %pi (plus N M P) %-> (plus (s N) M (s P)) %.

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

Using the STELF emacs mode

You use STELF by asking it to process declarations. STELF 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 STELF 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 STELF. 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:

STELF server: (default twelf-server) /something/bin/

This is asking which STELF 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

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

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

Hacks

If you use multiple frames with Emacs, twelf-mode annoyingly pops up the STELF 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).