Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-01 08:10:05 -0800 (Fri, 01 Jan 1999)
Revision: 2545
Log message:

      This is supposed to fix alpha_equal.
      Can somebody double-check me? Thanks.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-01-01 09:46:03 -0800 (Fri, 01 Jan 1999)
Revision: 2546
Log message:

      Fixed opname specification error in Itt_fset.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-01 09:51:22 -0800 (Fri, 01 Jan 1999)
Revision: 2547
Log message:

      This file produces different results with Term_ds and Term_std,
      even after alpha_equal is fixed.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-01-01 12:08:15 -0800 (Fri, 01 Jan 1999)
Revision: 2548
Log message:

      Fixed off-by-one error in nth_clause_addr.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-01-01 12:14:13 -0800 (Fri, 01 Jan 1999)
Revision: 2549
Log message:

      Fixed up "make clean" to remove more files.
      The directory should be like a new checkout afterwards.
      Enabled set_debug function in toploop.  You can
      turn on debugging with
      
      # set_debug "xxx" true;;
      
      for some debug variable xxx.
      

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 by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-01-02 09:04:32 -0800 (Sat, 02 Jan 1999)
Revision: 2551
Log message:

      Fixed some linking problems with intern/extern.c when Ensemble
      is not included.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-02 14:23:32 -0800 (Sat, 02 Jan 1999)
Revision: 2552
Log message:

      Fixed the build with undefined OCAMLSRC and the native code build
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-02 21:31:04 -0800 (Sat, 02 Jan 1999)
Revision: 2553
Log message:

      Added profiling control functions stop_gmon and restart_gmon to MP
      top loop. Now it is possible to get a "clean" profiling information
      that does not include any startup overhead.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-02 21:31:36 -0800 (Sat, 02 Jan 1999)
Revision: 2554
Log message:

      Forgot the main profiling file :-)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-02 23:24:51 -0800 (Sat, 02 Jan 1999)
Revision: 2555
Log message:

      Another small (~6%) PHP4 speedup
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-03 00:03:55 -0800 (Sun, 03 Jan 1999)
Revision: 2556
Log message:

      This is a little faster.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-04 16:37:27 -0800 (Mon, 04 Jan 1999)
Revision: 2557
Log message:

      Create ../lib/mbs-mpl.txt link on "make opt"
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-04 16:52:23 -0800 (Mon, 04 Jan 1999)
Revision: 2558
Log message:

      I've got test.opt to compile, but it would raise an exception when
      I try to run it, probably because I do not know how to
      call Sequent.create
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-04 17:17:51 -0800 (Mon, 04 Jan 1999)
Revision: 2559
Log message:

      Factorial example now works. To run:
      
      % ./mpopt
      # load "itt_test";;
      # cd "itt_test/fact650";;
      # refine timingT factT;;
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-01-05 20:11:59 -0800 (Tue, 05 Jan 1999)
Revision: 2560
Log message:

      Test function for itt_fset.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-01-05 20:12:23 -0800 (Tue, 05 Jan 1999)
Revision: 2561
Log message:

      Test function for refl_term.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-01-06 14:28:38 -0800 (Wed, 06 Jan 1999)
Revision: 2562
Log message:

      Added a dash in meta-prl.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-01-06 14:30:39 -0800 (Wed, 06 Jan 1999)
Revision: 2563
Log message:

      Removed redundant opens, indentation fix.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-01-08 13:51:02 -0800 (Fri, 08 Jan 1999)
Revision: 2564
Log message:

      This is the version of the distributed prover used in the
      CADE-16 original paper.  I'm still adjusting it though, so
      that we can use term_ds and native-code.
      
      If any of you have problems compiling clib/mmap.c, let me know.  It
      should compile on Linux and Win32, but we should put in stubs
      if there are problems on other systems.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-09 17:51:16 -0800 (Sat, 09 Jan 1999)
Revision: 2565
Log message:

      Fixed misleading comment
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-12 14:36:39 -0800 (Tue, 12 Jan 1999)
Revision: 2566
Log message:

      Set LC_ALL and LANG environment variables to "C" when creating
      mp_version.ml, so that the date in mp_version would always be in English
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-12 15:10:22 -0800 (Tue, 12 Jan 1999)
Revision: 2567
Log message:

      Suffix for the Refiner module to use.
      Possible values: ds_verb, ds_simp, std_verb, std_simp
      
      The system looks for suffix to use:
       1) In .refiner file (if it's non-empty)
       2) In MP_REFINER environment variable (if set)
       3) Prints warning and uses "ds_verb"
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-14 11:36:37 -0800 (Thu, 14 Jan 1999)
Revision: 2568
Log message:

      I believe, I've fixed the problem Yegor had found.
      
      The bug was not in == comparisons, but in compare_params
      function, where some indices were wrong.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 1999-01-15 02:00:56 -0800 (Fri, 15 Jan 1999)
Revision: 2569
Log message:

      
      CVS:
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-01-15 16:43:16 -0800 (Fri, 15 Jan 1999)
Revision: 2570
Log message:

      Added smaller examples.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-16 18:28:45 -0800 (Sat, 16 Jan 1999)
Revision: 2571
Log message:

      A Quick Guide to MetaPRL Profiling
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 1999-01-17 00:09:25 -0800 (Sun, 17 Jan 1999)
Revision: 2572
Log message:

      
      
      Alternate version of Term_copy with Alesha'a "fast" algorithm.
      Not tested yet.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-01-25 10:21:31 -0800 (Mon, 25 Jan 1999)
Revision: 2573
Log message:

      Distributed refiner for CADE-16.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-01-25 10:34:13 -0800 (Mon, 25 Jan 1999)
Revision: 2574
Log message:

      Added edit_set_goal, which loads the package if it is not yet loaded.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-01-25 11:23:08 -0800 (Mon, 25 Jan 1999)
Revision: 2575
Log message:

      Added edit_save function to save a specific package.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-27 19:57:07 -0800 (Wed, 27 Jan 1999)
Revision: 2576
Log message:

      Added some simple code to match two hypothesis lists.
      It does not always do the right thing, but would probably
      succeed in many cases
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-01-28 10:44:05 -0800 (Thu, 28 Jan 1999)
Revision: 2577
Log message:

      Upgraded to OCaml 2.01.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-28 14:53:13 -0800 (Thu, 28 Jan 1999)
Revision: 2578
Log message:

      Fixed some of "this expression should have type unit" warnings
      

Changes by: Lori Lorigo (lorigo at sbcglobal.net)
Date: 1999-01-29 09:26:07 -0800 (Fri, 29 Jan 1999)
Revision: 2579
Log message:

      Upgraded to OCaml 2.01.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-01-31 13:42:08 -0800 (Sun, 31 Jan 1999)
Revision: 2580
Log message:

      Added "simp" and "verb" rules to Makefiles.  There are no *.mlp and *.mlip
      files in the refiner any longer.  Instead, the C-preprocessor is run at
      compile time.
      
      By default, the verbose refiner is generated.  To get the others, use
      make simp, or make opt_simp.