Changes by: Stephan Schmitt (sschmitt at sapient.com)
Date: 2000-02-02 10:19:32 -0800 (Wed, 02 Feb 2000)
Revision: 2880
Log message:

      *** empty log message ***
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-10 00:58:48 -0800 (Thu, 10 Feb 2000)
Revision: 2882
Log message:

      Updated the CVS documentation URL.
      
      BTW, the new documentation page includes a nice CVS Quick Reference -
      http://www.sourcegear.com/CVS/Docs/ref
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-15 16:31:35 -0800 (Tue, 15 Feb 2000)
Revision: 2883
Log message:

      Enabled the "strict" rewriter mode.
      
      In "strict" mode, <<lambda{x.'t}>> will only match terms where "t" does not contain
      free occurences of "x" while <<lambda{x.'t['x]}>> will match any lambda expression.
      In "relaxed" mode both redices will match any lambda expression.
      
      This is done
      1) To force rule authors to completely specify the binding structure
      2) To allow rule authors to specify free variables restrictions easier
      
      refiner/refiner/refine.ml, filter/boot/rewrite_boot.ml and theories/tactic/tactic_cache.ml
      use the strict mode.
      
      filter/base/filter_prog.ml uses relaxed mode for d.f. and compiles ml rewrites
      using the strict mode
      
      refiner/reflib/dform.ml, refiner/reflib/term_dtable.ml and refiner/reflib/term_match_table.ml
      use the relaxed mode.
      
      Please let me know if this change breaks something.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-17 14:05:25 -0800 (Thu, 17 Feb 2000)
Revision: 2884
Log message:

      Now z.ml runs again
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-17 14:13:44 -0800 (Thu, 17 Feb 2000)
Revision: 2885
Log message:

      Fixed the jtest function
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-17 14:44:34 -0800 (Thu, 17 Feb 2000)
Revision: 2886
Log message:

      Now ``cd "/theory"'' also initializes the theory, so there is no need
      to do ``ls ""'' before being able to type in terms and use the theory.
      
      P.S. There is probably a better way to this, so I marked it as HACK.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-17 15:04:30 -0800 (Thu, 17 Feb 2000)
Revision: 2887
Log message:

      Some .mlz files were not marked as such in Makefiles - fixed
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-17 17:01:54 -0800 (Thu, 17 Feb 2000)
Revision: 2888
Log message:

      Moved all the test files to the tests directory to keep things cleaner
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-17 19:26:38 -0800 (Thu, 17 Feb 2000)
Revision: 2889
Log message:

      - When compiling a MetaPRL file referenced using its path instead of
      just a name, only the basename is now used as the theory name.
      This allowed me to put some MetaPRL files into a separate directory
      without having to give them their own Makefile and still be able
      to cd the theories produced by those files.
      However, that "separate directory" still has to be added to the
      include pacth (using the -I command) in order for this to work.
      
      - Added a new mk/config variable TESTS that specifies whether to compile
      various test theories (itt_test, test, prop-pigeon) into MetaPRL.
      By default it is set to "no".
      
      - Added the prop-pigeon theory and put the pigeon2 - pigeon9 theorems there.
      I still have to recover pigeonT from the CVS repository and fix propDecideT
      to be able to test these.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-17 20:30:36 -0800 (Thu, 17 Feb 2000)
Revision: 2890
Log message:

      Restored the old code for proving the propositional pigeon-hole principle.
      For some reason the proveT tactic does not get exported properly,
      so p4.ml still does not work.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-18 19:33:01 -0800 (Fri, 18 Feb 2000)
Revision: 2891
Log message:

      Renamed
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-18 19:45:48 -0800 (Fri, 18 Feb 2000)
Revision: 2892
Log message:

      These are obsolete.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-18 20:13:58 -0800 (Fri, 18 Feb 2000)
Revision: 2893
Log message:

      Fixed the "profile" target in the Makefile. I still have to fix my Ocaml
      patches in order to get "make profile" to work again.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-18 20:14:54 -0800 (Fri, 18 Feb 2000)
Revision: 2894
Log message:

      Prefixed the Failure messages with the module name.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-18 20:27:52 -0800 (Fri, 18 Feb 2000)
Revision: 2895
Log message:

      Fixed a bug in the "Strict" rewriter mode.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-19 18:07:03 -0800 (Sat, 19 Feb 2000)
Revision: 2896
Log message:

      .
      

Changes by: Vladimir N. Krupski (krupski at lpcs.math.msu.su)
Date: 2000-02-20 05:16:33 -0800 (Sun, 20 Feb 2000)
Revision: 2897
Log message:

      tptp_prove1.ml* is a copy of tptp_prove.ml* with old unification replaced
      strightforwardly by the new correct one -- unify_mm. No optimization of
      the calls (but it should be done next).
      

Changes by: Vladimir N. Krupski (krupski at lpcs.math.msu.su)
Date: 2000-02-20 06:00:19 -0800 (Sun, 20 Feb 2000)
Revision: 2898
Log message:

      I switch off the error messages produced by old unification.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-20 16:04:25 -0800 (Sun, 20 Feb 2000)
Revision: 2899
Log message:

      - Fixed the prop-pigeon tactics.
      The solution was to wrap dT with thinningT false
      
      - Added the test files for all the prop-pigeon test we are using.
      
      - Made sure "make clean" in editor/ml also cleans editor/ml/tests
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-21 15:11:58 -0800 (Mon, 21 Feb 2000)
Revision: 2900
Log message:

      When a list of subgoals is too big, displaying used to take a while. I implemented a
      workaround - to only display subgoals when there are <20 of them. We'll need to
      find a better solution - in particular we should take into account subgoal sizes, not only
      the number of subgoals.
      
      It may be a good idea to implement a generic display-form mechanism to allow limiting
      the number of lines a sertain term would occupy. On the other hand, such an approach
      would only save the time to output the display form, but not the time to produce it.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-21 16:40:43 -0800 (Mon, 21 Feb 2000)
Revision: 2901
Log message:

      Added profiling comtrol to some tests
      
      Added explicit include of the mk/preface to some Makefiles
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-21 17:47:43 -0800 (Mon, 21 Feb 2000)
Revision: 2902
Log message:

      Small bugfixes
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-21 20:09:08 -0800 (Mon, 21 Feb 2000)
Revision: 2903
Log message:

      - The strict rewriter mode allowed me to replace the ml_rule thin with an ordinary
      rule. I believe this should make thinT faster, but for some reason it does not happen.
      
      - Disabled the http server for now
      
      - Mp_big_int errors should be Invalid_arguments, not failures
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-21 20:58:53 -0800 (Mon, 21 Feb 2000)
Revision: 2904
Log message:

      When building contractum we used to build a new operator each time we wanted
      to construct a new term. Now we only do that if the operator of the original
      rule contractum had meta-parameters, otherwise we can simply use the operator
      from the rule contractum.
      
      The reason we want to have this optimization is that since we do opname lookups
      very often, we want to have fewer operators so that they could sit in CPU cache.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-21 21:39:46 -0800 (Mon, 21 Feb 2000)
Revision: 2905
Log message:

      Added a new function for free variable testing.
      Renamed all the free variable testing functions for uniformity:
         val is_var_free : string -> term -> bool
         val is_some_var_free : string list -> term -> bool
         val is_some_var_free_list : string list -> term list -> bool
      
      Made Strict rewriter checking use is_some_var_free (speedup!).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2000-02-22 09:42:16 -0800 (Tue, 22 Feb 2000)
Revision: 2906
Log message:

      Itt_bool now expands.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-22 19:22:17 -0800 (Tue, 22 Feb 2000)
Revision: 2907
Log message:

      Fixed the ASCII files generation to correctly handle the situation
      when the previous version of the file had duplicate terms.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-23 14:00:06 -0800 (Wed, 23 Feb 2000)
Revision: 2908
Log message:

      Efficiency fixes.
      
      This makes p4.ml 3% faster and f650.ml 11% faster
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-23 15:21:09 -0800 (Wed, 23 Feb 2000)
Revision: 2909
Log message:

      Efficiency improvements.
      
      12% on p4.ml, 4% on f650.ml, 1% on tptp-gen.ml
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-23 15:48:00 -0800 (Wed, 23 Feb 2000)
Revision: 2910
Log message:

      Another 2% on p4.ml
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2000-02-23 17:42:53 -0800 (Wed, 23 Feb 2000)
Revision: 2911
Log message:

      Planning for update to .prla files.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2000-02-23 22:55:47 -0800 (Wed, 23 Feb 2000)
Revision: 2912
Log message:

      Most of the theories in Itt now expand without errors.
      One exception is Itt_fset, which will require some work.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-24 00:01:14 -0800 (Thu, 24 Feb 2000)
Revision: 2913
Log message:

      I hope I finally got it right
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-24 00:29:31 -0800 (Thu, 24 Feb 2000)
Revision: 2914
Log message:

      Moved the expand-itt test into tests directory
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-24 15:13:48 -0800 (Thu, 24 Feb 2000)
Revision: 2915
Log message:

      Efficiency: another 3% on f650.ml
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-24 16:20:24 -0800 (Thu, 24 Feb 2000)
Revision: 2916
Log message:

      There is no need to call dest_msequent when we only want the goal, but
      not the assumtions.
      
      Speedup: 2% in p4.ml
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-24 17:00:32 -0800 (Thu, 24 Feb 2000)
Revision: 2917
Log message:

      Efficiency: Another 6% on p4.ml
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-24 17:59:59 -0800 (Thu, 24 Feb 2000)
Revision: 2918
Log message:

      Scripts for running ultiple tests in a batch.