Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-01-02 08:47:14 -0800 (Sat, 02 Jan 1999)
Revision: 2550
Log message:

      Fixed some problems with Ensemble.
      The closure marshaler was marshaling huge closures containing
      Ensemble itself. I think I have fixed this problem.
      The performance numbers may change slightly due to a
      modification of thread_refiner_null, which now composes
      extracts only after an entire proof is done.
      

Changes  Path
+2 -1 metaprl/Makefile
+16 -2 metaprl/clib/Makefile
Added metaprl/clib/extern.c
Properties metaprl/clib/extern.c
Added metaprl/clib/extern.patch
Properties metaprl/clib/extern.patch
Added metaprl/clib/intern.c
Properties metaprl/clib/intern.c
Added metaprl/clib/intern.patch
Properties metaprl/clib/intern.patch
Added metaprl/clib/register.c
Properties metaprl/clib/register.c
Properties metaprl/debug
Added metaprl/debug/Makefile
Properties metaprl/debug/Makefile
Added metaprl/debug/debug.ml
Properties metaprl/debug/debug.ml
Added metaprl/debug/debug.mli
Properties metaprl/debug/debug.mli
Added metaprl/debug/debug_symbols.ml
Properties metaprl/debug/debug_symbols.ml
Added metaprl/debug/debug_symbols.mli
Properties metaprl/debug/debug_symbols.mli
+1 -0 metaprl/editor/ml/.gdbinit
+23 -25 metaprl/editor/ml/Makefile
+1 -1 metaprl/editor/ml/mpconfig
+1 -0 metaprl/editor/ml/shell_mp.ml
+0 -0 metaprl/editor/ml/test.ml
+1 -1 metaprl/editor/ml/w.ml
+0 -1 metaprl/editor/ml/y.ml
+16 -13 metaprl/ensemble/Makefile
+8 -3 metaprl/ensemble/appl_closure.ml
+5 -4 metaprl/ensemble/appl_closure.mli
+49 -6 metaprl/ensemble/ensemble_queue.ml
+32 -17 metaprl/ensemble/remote_ensemble.ml
Added metaprl/ensemble/remote_monitor.ml
Properties metaprl/ensemble/remote_monitor.ml
Added metaprl/ensemble/remote_monitor.mli
Properties metaprl/ensemble/remote_monitor.mli
+21 -5 metaprl/ensemble/remote_null.ml
+9 -5 metaprl/ensemble/remote_sig.mlz
+7 -4 metaprl/ensemble/thread_refiner.mli
+149 -53 metaprl/ensemble/thread_refiner_ens.ml
+7 -4 metaprl/ensemble/thread_refiner_ens.mli
+6 -4 metaprl/ensemble/thread_refiner_ens_mod.ml
+52 -29 metaprl/ensemble/thread_refiner_null.ml
+7 -4 metaprl/ensemble/thread_refiner_null.mli
+6 -4 metaprl/ensemble/thread_refiner_null_mod.ml
+22 -8 metaprl/ensemble/thread_refiner_sig.mlz
+1 -1 metaprl/filter/filter_ast.ml
+1 -1 metaprl/filter/filter_cache.ml
+2 -2 metaprl/mk/config
Properties metaprl/mllib
+3 -2 metaprl/mllib/Makefile
Deleted metaprl/mllib/ctype.ml
Deleted metaprl/mllib/ctype.mli
Added metaprl/mllib/mp_ctype.ml
Properties metaprl/mllib/mp_ctype.ml
Added metaprl/mllib/mp_ctype.mli
Properties metaprl/mllib/mp_ctype.mli
Added metaprl/mllib/register.mlz
Properties metaprl/mllib/register.mlz
+5 -4 metaprl/mllib/remote_lazy_queue.ml
+5 -4 metaprl/mllib/remote_lazy_queue_sig.ml
+30 -12 metaprl/mllib/remote_queue_null.ml
+8 -4 metaprl/mllib/remote_queue_sig.ml
+12 -12 metaprl/refiner/term_ds/term_base_ds.mlp
+14 -14 metaprl/refiner/term_std/term_base_std.mlp
+171 -76 metaprl/theories/tactic/tactic_type.ml
+1 -0 metaprl/theories/tactic/tactic_type.mli
+1 -1 metaprl/theories/tactic/var.ml