ViewVC logotype

Log of /metaprl/theories/tactic/Conscript

Parent Directory Parent Directory | Revision Log Revision Log

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

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: 804 byte(s)
Diff to previous 3532
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 3532 - (view) (download) (annotate) - [select for diffs]
Modified Sun Mar 10 23:29:54 2002 UTC (19 years, 3 months ago) by nogin
File length: 761 byte(s)
Diff to previous 3449
I am committing David Bustos' changes to the cons build system for Metaprl.

See David's message "cons for MetaPRL" in the newsgroup for more information -

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: 949 byte(s)
Diff to previous 3410
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 3410 - (view) (download) (annotate) - [select for diffs]
Added Tue Sep 25 16:52:43 2001 UTC (19 years, 8 months ago) by nogin
File length: 897 byte(s)
- Merged the Ocaml 3.02 changes

- Now http server is compiled in by default, but is only started if
the "-http true" argument is passed or MP_HTTP environment variable
is set to "true".

- A few other minor changes.

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