Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-08-17 08:28:26 -0700 (Mon, 17 Aug 1998)
Revision: 2440
Log message:

      Added multithreaded refinement.  NOTE: this requires a patch to
      LinuxThreads.  The patched library is in clib/libpthreads-i386-linux.lib.
      I'll add the source level patch in the next release.
      
      Removed failure caching from tptp_prove to get more deterministic
      refinements.  Modified Tptp_prove.testT to create a single proof
      goal, rather than running proveT several times.
      

Changes  Path
+9 -3 metaprl/clib/Makefile
Added metaprl/clib/getrusage.c
Properties metaprl/clib/getrusage.c
Binary metaprl/clib/libpthread-i386-linux.lib
Properties metaprl/clib/libpthread-i386-linux.lib
+3 -4 metaprl/editor/ml/Makefile
+1 -1 metaprl/editor/ml/test.ml
+1 -1 metaprl/editor/ml/test.mli
Added metaprl/editor/ml/w.ml
Properties metaprl/editor/ml/w.ml
+4 -0 metaprl/editor/ml/y.ml
+2 -2 metaprl/mk/config
+1 -0 metaprl/mllib/Makefile
Added metaprl/mllib/getrusage.ml
Properties metaprl/mllib/getrusage.ml
Added metaprl/mllib/getrusage.mli
Properties metaprl/mllib/getrusage.mli
+6 -2 metaprl/theories/tactic/Makefile
Added metaprl/theories/tactic/remote_null.ml
Properties metaprl/theories/tactic/remote_null.ml
Added metaprl/theories/tactic/remote_null.mli
Properties metaprl/theories/tactic/remote_null.mli
Deleted metaprl/theories/tactic/remote_refiner.ml
Deleted metaprl/theories/tactic/remote_refiner.mli
Added metaprl/theories/tactic/remote_sig.mlz
Properties metaprl/theories/tactic/remote_sig.mlz
+28 -10 metaprl/theories/tactic/tactic_type.ml
Added metaprl/theories/tactic/thread_event.ml
Properties metaprl/theories/tactic/thread_event.ml
Added metaprl/theories/tactic/thread_event.mli
Properties metaprl/theories/tactic/thread_event.mli
Added metaprl/theories/tactic/thread_refiner.ml
Properties metaprl/theories/tactic/thread_refiner.ml
Added metaprl/theories/tactic/thread_refiner.mli
Properties metaprl/theories/tactic/thread_refiner.mli
+0 -26 metaprl/theories/tactic/thread_refiner_sig.mlz
Deleted metaprl/theories/tactic/thread_refiner_tree.ml
Deleted metaprl/theories/tactic/thread_refiner_tree.mli
Added metaprl/theories/tactic/thread_util.ml
Properties metaprl/theories/tactic/thread_util.ml
Added metaprl/theories/tactic/thread_util.mli
Properties metaprl/theories/tactic/thread_util.mli
+67 -42 metaprl/theories/tptp/tptp_prove.ml
+1 -1 metaprl/util/ocamldep.mll