ViewVC logotype

Log of /metaprl/editor/ml/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: 3953 byte(s)
Diff to previous 3562
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 3562 - (view) (download) (annotate) - [select for diffs]
Modified Wed Apr 3 08:37:31 2002 UTC (19 years, 2 months ago) by emre
File length: 3436 byte(s)
Diff to previous 3540
So, I've defined the compile function in Mp_mc_compile to actually
take an Fir.prog, convert the function definitions to terms,
and then back again, in one big identity operation.  The current
term representation of the FIR functions is a bit of a hack that
will need to be cleaned up if anything non-trivial is to be done.
(Each individual function is fine I hope.  It's the program as a whole
that's represented rather poorly.  It's essentially a (term SymbolTable.t),
one term for each fundef in the original Fir.prog.prog_funs.)
Though, this should be sufficient for basic testing I think.

Revision 3540 - (view) (download) (annotate) - [select for diffs]
Modified Mon Mar 11 16:03:51 2002 UTC (19 years, 3 months ago) by emre
File length: 3418 byte(s)
Diff to previous 3533
Updated theories/mc/Makefile to
reflect new file names (oops!).
Changed editor/ml/Conscript to use a more
appropriate mechanism for declaring the
hidden dependencies of mpopt.

Revision 3533 - (view) (download) (annotate) - [select for diffs]
Modified Mon Mar 11 09:54:10 2002 UTC (19 years, 3 months ago) by emre
File length: 3412 byte(s)
Diff to previous 3532
I've renamed theories/mc/fir_eval to use my
(attrocious) prefix so that a file name collision
with fir_eval in the MC source tree doesn't happen.
Other files in theories/mc have been changed

I've renamed mp_mc_theory to just use a .mlz
file since the .ml and .mli files were the
exact same and it's a hassle to modify them
both whenever they need to be changed.

I've updated editor/ml/Conscript so that mpopt
actually includes the Itt_theory and Mp_mc_theory.
This makes it much more useful.

mc/Conscript has been updated to reflect new code
in the MC source tree.

After this, MetaPRL should compile with the
main trunk of the MC source tree if the MC_ROOT
environment variable is set appropriately.

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: 3388 byte(s)
Diff to previous 3477
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 3477 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jan 18 16:35:35 2002 UTC (19 years, 5 months ago) by emre
File length: 3167 byte(s)
Diff to previous 3472
1. Re-exported fir_eval.prla.
2. Mc_set : minor display form change.
3. Randomly reformatted some Conscripts it seems.
   (I removed tab characters from the files.)

The next steps will be to:
1. Consider renaming all files in theories/mc
   to start with mp_ or some other "unique" prefix
   so that the naming is consistant
   and avoids conflicts with files in MC.
2. Begin testing the mc_fir_connect code.  This
   will probably take some time to get completely

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: 1849 byte(s)
Diff to previous 3457
-  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 3457 - (view) (download) (annotate) - [select for diffs]
Modified Wed Nov 28 09:46:07 2001 UTC (19 years, 6 months ago) by emre
File length: 3167 byte(s)
Diff to previous 3454
- Continuing implementation of code to convert from Fir.prog to MetaPRL terms,
  and vica versa.
- Renamed some files to avoid conflicts.

Revision 3454 - (view) (download) (annotate) - [select for diffs]
Modified Wed Nov 21 09:17:04 2001 UTC (19 years, 7 months ago) by emre
File length: 3238 byte(s)
Diff to previous 3449
Updates to solve some build problems:

make : Building with make is completely independent of the presence
   of the Mojave compiler source tree, since the MC compiler must
   be built with cons.  Thus, the only code that currently depends
   on MC, theories/mc/fir_marshal is not compiled.  Not including
   it as a part of the build of theories/mc is not a problem since it
   has no logical or otherwise meaningful content beyond the functions to
   convert between terms and the Fir.prog data structure of the compiler,
   i.e. this present no loss to the mc theory.

cons : If the MC_ROOT environment variable is defined, its assumed to point
   to the root directory of the Mojave compiler source tree, and in this
   case, we build the two source trees together.  (To use MC, you need
   to define MC_ROOT anyway, so there's no need to put it as a config
   option somewhere.)  In particular, we (will) compile the
   "connection" code in theores/mc/fir_marshal.  If MC_ROOT is undefined,
   MetaPRL will build almost identically; the only difference is that
   fir_marshal is not compiled in.

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: 3340 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: 1742 byte(s)
Diff to previous 3439
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 3439 - (view) (download) (annotate) - [select for diffs]
Modified Sun Nov 4 19:38:36 2001 UTC (19 years, 7 months ago) by emre
File length: 1738 byte(s)
Diff to previous 3410
Changes to get the mc theory compiled in by default.

Revision 3410 - (view) (download) (annotate) - [select for diffs]
Added Tue Sep 25 16:52:43 2001 UTC (19 years, 9 months ago) by nogin
File length: 1679 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