The first step in getting started with Lego is to set an environment variable specifying which version is desired. There are several versions of Lego available; some are essentially alpha test versions of new extensions, so are not the best for beginners. The version we want is called "cafr", so you should put the following line in your .benv file in your home directory:
export LEGOVERSION=cafr
(You may have to create the file .benv; this file is executed every time a shell starts in a new environment.)
This choice will not take effect unless you now logout and login again; however, for today the default version will be fine.
Create a directory called lego in your home directory. Copy the file example.l into your lego directory. (The full path for this file on CS machines /home/lego/pub/html/CAFR/96-97/example.l.) Now edit this file with xemacs.
Xemacs will automatically load a special mode for Lego files if the file extension is ".l". The first line of the example file creates a module called "example", and specifies that it imports another module called "lib_logic". All commands are terminated by a semicolon.
If you press the third mouse button, you will get a popup menu of Lego commands. Choose "Start LEGO".
Lego will start in another buffer. The two buffers communicate, so that you can type commands in your own file and send them to the Lego process. You can do this via the menu, or directly with some shortcuts. Of course, you can type directly to lego as well if you wish, but your commands will not be saved in a file.
First, process the whole buffer, either by selecting this option from the menu or by typing ^c^b (that's control-c, control-b). This will load in the requested libraries and process all of the commands.
The lecture notes contain an explanation of what each step does in this example proof. To run through the first proof step-by-step, you can process each line in turn with ^c^j. Notice that this moves you automatically to the next line in the file.
If you try to process the second proof in the file in the same way, Lego will complain because it already has a proof called "example", which it saved the first time it went through the file. You can modify the name and step through this proof as well.
When you are typing your own proofs, it is nice to have Lego process your commands automatically, as you go along. To do this, you can choose "toggle active ;" from the menu (alternatively, type ^c ;). This will send each command to Lego as soon as you type the concluding semicolon.
Now you are ready to try your own proofs!
Judith Underwood