Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2001-11-19 07:09:10 -0800 (Mon, 19 Nov 2001)
Revision: 3449
Log message:
First working version with meta-prl/mc together.
To compile with mc, as of Mon Nov 19 07:04:50 PST 2001:
0. Get a copy of mc, available from mojave.cs.caltech.edu.
If you don't know how, you can ask jyh@cs.caltech.edu.
1. set the MC_ROOT environment variable to the root
directory for mc.
2. Compile using cons. You chould compile from the root
meta-prl directory first. After that, you can build
from the editor/ml directory (use cons -t).
There are still some problems with dependencies in theories/tactic.
prlc adds a lot of implicit dependencies, and I've only caught a few
of them. It compiles for now, but beware of "undefined modules" in
editor/ml.