next up previous contents
Next: The Input Language Up: Tutorial Previous: Building the Prover if

The Platform

MARK2 is implemented in SML/NJ (Standard ML of New Jersey) and Caml Light (another dialect of ML, which runs on PC's!)

To start the SML version from UNIX on onyx, first type


You will get some verbiage and an SML prompt.

The fact that we are in ML has two effects. One is that you will always issue commands at the ML prompt (a hyphen). Another is that ML will send you some messages (it reports the type of its output to you after each command). I don't know a way to suppress this.

The direct effect it has on you has to do with the syntax of command lines. Each prover function is actually an ML function. Those which have arguments take string arguments, which must be enclosed in double quotes (there are a couple of commands which take integer parameters; this will be pointed out). ML insists that those which do not have arguments take a dummy argument, written () and known affectionately as ``unit''. ML command lines must end with semicolons. In the Caml Light version, all command lines must end with two semicolons.

Sample command lines:

showalltheorems();  (* a command with no parameters *)

axiom "COMM" "?x+?y" "?y+?x";  (* a command with three string
arguments *)

If you goof up in ML, ML will send you error messages. There is no easy way to damage your theorem prover session by outraging ML; just ignore commands which lead to ML errors and try again.

To abort a line and start over, type Control-C. To leave ML altogether, type Control-D. If Control-C is typed to break out of one of the command interpreters (execute, steps, or onestep) be sure to use the top command to reset environment variables.

To save your work in MARK2 in a new ``theory file'', type

storeall "<name of theory>";

Theory files have the extension ``.thy3'', added automatically by the ``storeall'' command. To open an existing theory file, issue the command

load "<name of theory>";  (* don't include the .thy3 extension! *)

A lot of stuff will happen; you may have to wait a little while if the theory file is large.

If you have introduced a theory name by using either of the above commands, the command


will automatically save your work to the correct file.

next up previous contents
Next: The Input Language Up: Tutorial Previous: Building the Prover if

Randall Holmes
Fri Sep 5 16:28:58 MDT 1997