ViewVC logotype

Log of /metaprl/refiner/reflib/Conscript

Parent Directory Parent Directory | Revision Log Revision Log

Sticky Revision:
(Current path doesn't exist after revision 4552)

Revision 3576 - (view) (download) (annotate) - [select for diffs]
Modified Fri Apr 12 05:37:53 2002 UTC (19 years, 2 months ago) by emre
File length: 1291 byte(s)
Diff to previous 3449
These updates to the Conscripts allow for a compiles,
started in the MC source tree, to optionally
compile MetaPRL.  Nothing in MetaPRL itself should be
affected by these changes.  The only important
thing to note that is "#", in INCPATH's
has been replaced by $env->{MP}, which is set
in the toplevel Conscript.  "#" will refer to the
wrong root if the compile is started in MC.

Revision 3449 - (view) (download) (annotate) - [select for diffs]
Modified Mon Nov 19 15:09:10 2001 UTC (19 years, 7 months ago) by jyh
File length: 1321 byte(s)
Diff to previous 3363
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

Revision 3363 - (view) (download) (annotate) - [select for diffs]
Added Tue Aug 7 20:32:03 2001 UTC (19 years, 10 months ago) by jyh
File length: 1291 byte(s)
Added some initial Conscript files.  cons is a "make" replacement.
make will continue to work in the usual way, but cons will
eventually make it easier to produce a build.

This form allows you to request diffs between any two revisions of this file. For each of the two "sides" of the diff, enter a numeric revision.

  Diffs between and
  Type of Diff should be a

  ViewVC Help
Powered by ViewVC 1.1.26