Twelf without Emacs

From The Twelf Project
Jump to: navigation, search

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 make other.cfg

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 loadFile sometwelf.elf

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: Solving... N = s (s (s z)). More? You can exit the logic programming top-level by pressing Ctrl-C.

Quitting

To quit from the Twelf server, type quit or press Ctrl-D.