Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-07 19:11:12 -0800 (Mon, 07 Nov 2005)
Revision: 8127
Log message:

      (Issue 543) Compute the full list of theories to build based on the
      inter-theory dependencies.
      
      Now that ITT is composed of a bunch of smaller subtheories, having to specify
      the full list of theories in mk/config became more annoying. This commit
      implements the notion of theory dependencies and uses it to compute the full
      list of theories to be compiled. Now setting THEORIES in mk/config to
      something like "poplmark/naive" should work, bringing in all the necessary
      dependencies.
      
      In order to work correctly, the theory/*/OMakefile:
      
      - MAY define or update the THEORY_DEPENCIES variable. This variable MUST
        contain an array of theory "names" (as before, the theory "name" is the
        directory name relative to $(ROOT)/theories). By default, THEORY_DEPENCIES
        is equal to "base"
      
      - SHOULD use either the Theory function (which takes a file list as an
        argument), or a VirtualTheory function (this takes a list of subdirectories
        as an argument and should be used for "virtual" theories that only bring
        together sub-theories, but do not contain any modules). Note that
        VirtualTheory overrides the THEORY_DEPENCIES variable, so any additonal
        modifications to THEORY_DEPENCIES in virtual theories (which usually
        shouldn't be necessary) need to go after the VirtualTheory call.
      
      - SHOULD NOT change the OCAMLINCLUDES variable (except for non-theory
        directories). The standard "Theory" function now sets OCAMLINCLUDES based on
        the value of THEORY_DEPENCIES, and if the resulting value is incorrect, it
        is usually a very good indication that THEORY_DEPENCIES is also incorrect.
      
      - SHOULD NOT use .SUBDIRS to bring in other theories; it should use
        THEORY_DEPENCIES or VirtualTheory mechanism instead.