Object Dependencies and Ordering

A correct library  in Nuprl is one where every definition and theorem refers only to objects occurring previously in the library. Unfortunately, Nuprl does not guarantee that this property is maintained when functions are used that modify the library. For example, it is possible to create a circular chain of lemma references.

There is only one way to guarantee that a theory (or collection of theories) is correct. This is to load it (them, sequentially) using one of the load-fully functions described at the end of the last section. This will force a theorem's proof to be expanded before the theorem is loaded into the library, and so guarantee that proofs only reference theorems that occur previously in the library.

Loading without using these load-fully functions and then using check_objects or check_theory will not guarantee that the library is correct, since during the checking of a theorem, all later theorems will be present in the library and will retain the statuses they had when they were dumped. However it is recommended that one always preceed a load-fully check, by loading the relevant theories without expanding theorems, and then using check_objects or check_theory. There are two reasons for this. Firstly, just to check that all proofs do indeed expand properly. Secondly, the current load-fully functions will blithely continue loading a library after an error has occurred, often creating a cascade of further errors. This bad behaviour will be corrected in the near future.

Nuprl does do some dependency checking  with definitions. For example, if a definition is deleted then the status of any entry depending on these objects is set to bad.

Because of the general lack of dependency checking, a user must be careful to keep library objects correctly ordered or reloading may fail. The move  function can be used to repair incorrect orderings and ensure that objects occur before their uses.

Here is a list of some of the main object dependencies  one should be aware of:

• Theorems on other theorems. Each theorem should only depend on theorems occurring earlier in the library. Note that several kinds of theorems are referenced automatically  by Nuprl tactics. For example, well-formedness theorems  (theorems whose names end in _wf  ) and various support lemmas used by the rewrite package.

• Theorems on abstractions. A theorem shouldn't refer to an abstraction before it is defined.
• Abstractions on abstractions. The right-hand-side of an abstraction should only refer to abstactions defined earlier in the library. Note that abstractions should not be recursive.
• ML objects on theorems, abstractions and other ML objects ML objects frequently assume the existence of certain theorems and abstractions. For example, one might include in an ML object a rewrite tactic which references a set of lemmas. One should always consider the introduction of such dependencies carefully. Continuing the example, if one were to change one of the lemmas would one want the rewrite tactic to automatically use this change? Many functions which access objects in the library can be written in a lazy fashion, such that they look up the object, only when they are called. Such functions however might be considerably less efficient than ones which do need to do a fair amount of preprocessing. Ideally, one wants to just do this preprocessing once. Below we discuss the use of caches  to resolve this partial evaluation problem.
• Theorems on ML objects Theorems can be proved using tactics and other ML functions defined in ML objects, so needless to say, those theorems should occur later in the library than the ML objects they are dependent on.

In addition, there are other dependencies one should be aware of:

• ML files on theories. It is desirable to be able to compile all ML files without having to have all theories a-priori loaded, so in general any dependencies should be of the lazy variety as explained earlier. It is a very bad idea to have compiled ML files dependent on functions defined in ML objects; whenever an ML function is compiled, it is timestamped  , and references between ML functions keep track of these timestamps. All functions in ML objects are compiled afresh every time the objects are loaded, so if one were to load ML files compiled in an earlier session, one could have stale function references which would result in ML crashing.
• Theories on ML files This is fine. We will soon be extending the theory mechanism so that one can specify optional ML files to only be loaded when certain theories are loaded.
• Cache Dependencies  . The ML tactic system maintains a fair amount ofstate  , much in the form of preprocessed lemmas  . We have an incremental update strategy for many of these caches to ensure that they track changes in the library state, so for most purposes these caches are invisible to the user. However, to date, not all the code for caches has been updated to use this incremental strategy, so for example, one might run into situations where the system refuses to acknowledge that one has added a missing lemma. In these situations, executing the function reset_caches : unit -> unit  might help. Caches are discussed in Chapter .