New Implementation of Mark2

Here is the SML source of the new implementation.

Facilities of the old implementation which are not present in the new but which are seldom if ever used at present are user-defined precedence and the "functional programming" features (these features have since been added, but are still not often used).. A major aim of the reimplementation is the installation of a more efficient system for keeping track of different kinds of dependencies, which, it is hoped, will allow reaxiomatization, redefinition, and theorem export facilities to be made usable in practice (this has now been put into practice for forget and theorem export)

The files for the new version are mirrored in my home directory at the University of Idaho: the source is "design", the executable is "Watson", and all the .wat files below are found there, and the corresponding saved theory files (with extension .sav.wat) have been built there. I plan to rebuild these each time I upgrade the executable significantly. The new version is functionally similar but not identical to the current implementation. There follows a list detailing points of difference:

Find here a Postscript file for the paper/documentation under construction.

Here are the Watson scripts. Be aware that Watson and the last release of Mark2 are not perfectly compatible; scripts to be run with the last release of Mark2 are found below.

Here is the new Watson page Here is the old Mark2 page.