Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-21 19:48:11 -0800 (Sat, 21 Jan 2006)
Revision: 8564
Log message:
In the theory search (OMakefile_theories.find-theory), do not
find the theory unless the MetaprlInfo file exists.
The issue is as follows. The THEORY_DEPS variable specifies
theories relative to the theories/ directory. So this requires
that we place theories in some place where the path works.
For example, I want my private theory to include these theories:
itt/reflection
poplmark/naive
This means I *must* name these directories as such (with
the current scheme), I can't just put them somewhere
myproject/reflection
myproject/naive
Instead, they must be something like
myproject/itt/reflection
myproject/poplmark/naive
Oh well. But if I define myproject/itt, this *does not* define the
itt theory. So the theory-path-search matches only if the MetaprlInfo
file exists.
With this, the search really is MetaPRL-specific. While I think that
this might still be a general problem, perhaps Aleksey's solution is
the right way to go. That is, we would keep a Map that would cache the
search-path results.
Changes | Path |
+8 -2 | metaprl/OMakefile_theories |
+0 -8 | metaprl/theories/itt/MetaprlInfo |
+8 -0 | metaprl/theories/itt/reflection/MetaprlInfo |