Twelf without Emacs
First, you should read up on Twelf with Emacs, to understand how Twelf programs are divided up into files and how one interacts with those files. Then, instead of using emacs, you can run the twelf-server command directly from your shell and interact with your files using the following commands. (You may find it convenient to run twelf-server under some readline wrapper program like rlwrap or ledit to get command-line editing and history.)
Loading the configuration file
To read your current config from sources.cfg, type
make To read some other config other.cfg, type
Checking an individual declaration
To check an individual declaration, type
readDecl Then, on a new line, type a Twelf declaration, terminated with a period.
Checking an individual file
To load an individual file sometwelf.elf, type
Logic programming proof search
To animate your specifications by doing logic programming queries, type
top You will be presented with a a prompt,
?- at which you can type queries with existential metavariables, like
?- plus (s z) (s (s z)) N. Assuming you've loaded the signature from the Natural numbers article), the Twelf server responds with the following:
N = s (s (s z)).
You can exit the logic programming top-level by pressing Ctrl-C.
To quit from the Twelf server, type
quit or press Ctrl-D.