ViewVC logotype

Log of /metaprl/Conscript

Parent Directory Parent Directory | Revision Log Revision Log

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

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: 3114 byte(s)
Diff to previous 3551
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 3551 - (view) (download) (annotate) - [select for diffs]
Modified Sun Mar 31 02:48:35 2002 UTC (19 years, 2 months ago) by emre
File length: 2881 byte(s)
Diff to previous 3532
Test cases for the "connection" code are pretty much complete.
I've fixed a few bugs that cropped up (including a major one
in Mp_mc_term_op).  What's needed now is the final set of functions
to take an entire MC Fir.prog to some sort of MetaPRL term.

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: 2847 byte(s)
Diff to previous 3482
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 3482 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jan 28 09:59:33 2002 UTC (19 years, 4 months ago) by emre
File length: 2767 byte(s)
Diff to previous 3478
Adding test cases for the MC connect code.
Slight change to INCPATH in Conscript to ensure
that the MC std. lib. is included first
(if we're compiling with MC).

Revision 3478 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jan 22 23:38:59 2002 UTC (19 years, 5 months ago) by emre
File length: 2767 byte(s)
Diff to previous 3472
1) The main Conscript has been modified.  Added lines for CPP so that MC
   compiles properly from MetaPRL.
2) Renamed some files in theories/mc/ so as to not confliced with
   files in MC.  I've chosen the (arguably atrocious) prefix
   of mp_mc_.

Assuming string_util.ml and rformat.ml, in the MC source tree,
are renamed to something else and the changes propagated as
necessary, this commit should re-enable MetaPRL and MC to build together
(using cons).

Revision 3472 - (view) (download) (annotate) - [select for diffs]
Modified Sat Dec 22 05:43:27 2001 UTC (19 years, 6 months ago) by emre
File length: 2609 byte(s)
Diff to previous 3449
-  Removed util/Construct since it seems to be
   unnecessary for building MetaPRL with cons.
-  Minor changes to other Conscript(s).
   Mostly formatting (changing tabs to spaces).
-  Top level Conscript only uses the MC std. lib.
   if MC_ROOT is defined.  Before, if MC_ROOT wasn't
   defined, the -I cmd. line arguments would have
   unnecessary things like -I /lib/naml/...
-  Minor changes to display forms in theories/mc.
-  Minor changes to code formatting in theories/mc.
-  Filled in missing Mc_fir_connect_* functions.
   I need to look over them at some point for
   obvious typo-bugs and perform other testing.

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: 2258 byte(s)
Diff to previous 3440
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 3440 - (view) (download) (annotate) - [select for diffs]
Modified Mon Nov 5 02:36:58 2001 UTC (19 years, 7 months ago) by nogin
File length: 2110 byte(s)
Diff to previous 3436
cons files:
- The mp_version.ml file is now created with a proper version string
- The refiner used is now controlled  by the RFEINER and TERM variables
specified in the top-level Conscript (but not yet taken from mk/config).

Revision 3436 - (view) (download) (annotate) - [select for diffs]
Modified Sat Nov 3 19:33:42 2001 UTC (19 years, 7 months ago) by emre
File length: 2113 byte(s)
Diff to previous 3434
Fixed a build error with cons.
(util needed to be built first.)

Revision 3434 - (view) (download) (annotate) - [select for diffs]
Modified Sat Nov 3 15:15:53 2001 UTC (19 years, 7 months ago) by jyh
File length: 2097 byte(s)
Diff to previous 3410
Added mc directory.

Revision 3410 - (view) (download) (annotate) - [select for diffs]
Modified Tue Sep 25 16:52:43 2001 UTC (19 years, 9 months ago) by nogin
File length: 2083 byte(s)
Diff to previous 3363
- 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.

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: 1755 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