Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-11-01 20:13:41 -0800 (Sat, 01 Nov 2003)
Revision: 5065
Log message:

      hopefully this will fix the problem
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-11-02 18:34:53 -0800 (Sun, 02 Nov 2003)
Revision: 5066
Log message:

      Fixed the second ingredient of the difference in behavior with Term_ds and Term_std:
      One place in arith.ml was still using simple equality to compare terms. Because of it arith.ml produced result that revealed some imperfect logic in itt_int_arith (was fixed yesterday).
      I think this commit closes the issue completely.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-03 19:16:48 -0800 (Mon, 03 Nov 2003)
Revision: 5068
Log message:

      More MERLIN paper formatting fixes (last ones, hopefully):
      - Switched from one ACM style to another, and added conference
      and copyright footer as they requested.
      - Added one of "on the next page", "above", "on the left"
      to all the reffigure's.
      (This is needed since the sig-alternate style is pretty liberal with
      figure placement, and most of the figure references end up being "on the
      next page" ones).
      

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2003-11-04 11:31:47 -0800 (Tue, 04 Nov 2003)
Revision: 5069
Log message:

      Aleksey: Refine.nth_hyp (AKA nthAssumT) should raise RefineError,
      not Invalid_argument when assumption index is out of range.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-04 16:13:44 -0800 (Tue, 04 Nov 2003)
Revision: 5070
Log message:

      More tweaks towards 3.07 compatibility.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-04 18:15:05 -0800 (Tue, 04 Nov 2003)
Revision: 5071
Log message:

      Changing the order of arguments in apply_subst to make it easier to use
      it in functions like List.map.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-04 19:23:11 -0800 (Tue, 04 Nov 2003)
Revision: 5072
Log message:

      Fixing bug 104:
      
      It used to be the case that we could rely on sequent bindings not clashing
      with any other bindings. However, once we allow nested sequents this assumption
      can no longer be enforced. I've added a explode_sequent_and_rename function
      (in TermMan module) that would rename all the sequent bindings as needed
      to avoid clashes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-05 15:34:13 -0800 (Wed, 05 Nov 2003)
Revision: 5073
Log message:

      Made sure nested sequents are properly considered in alpha equality checking.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-11-05 16:01:58 -0800 (Wed, 05 Nov 2003)
Revision: 5074
Log message:

      
      
      Finlay I added support for the record renaming.
      
      I defined rename[a:t;b:t]{'r} operator.
      
      I also defined as_additive{'r} operator that
      renames "+"-> "*", "0"-> "1", "neg"->"inv"
      
      One can prove that if 'r is a ring then as_additive{'r} in a group.
      (This should be added to the typeinf resource).
      
      I have also a bunch of tactics for renaming.
      The main tactic is foldAdditiveT that replaces for example 'r^+ by as_additive{'r}^*, and so on.
      There is also unfoldAdditiveT that opposite to foldAdditiveT.
      These two tactics should be enough to apply group theorems to rings.
      The tactic useAdditiveWithAutoT = foldAdditiveT thenT autoT thenT unfoldAdditiveT thenT autoT
      should work in all simple cases.
      
      I'm not sure if I pick up the right names for the tactics and the operations. Let me know what you think.
      
      Now rings could be defined for example as
      
      RingSig={car:univ; *: car->car; + : car -> car; 1: car; 0:car; inv: car -> car }
      Ring={R:RingSig | isGroup{as_additive{'R}} and .... }
      
      You can also define
      isAdditiveGroup{'G} = isGroup{as_additive{'G}}
      but then you need to add to the reduce resource two reductions:
       isAdditiveGroup{rename_mul_add{'G}} <--> isGroup{'G}
       isGroup{rename_add_mul{'G}} <--> isAdditiveGroup{'G}
      
      Then foldAdditiveT will replace isAdditiveGroup{'R} by isGroup{as_additive{'R}}
      
      See more details in Itt_record_renaming and itt_quickref.txt.
      The documentation is not very good right now,  let me know if you have any questions.
      
      I will commit the proofs soon.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-11-06 11:21:55 -0800 (Thu, 06 Nov 2003)
Revision: 5075
Log message:

      In this branch I switching WeakMemo from incremental GCion to "full" GCion. Instead of multiplying mutexes/conditional variables I use lists of mutually recursive tables and weakmemo-users are responsible for keeping them correct.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-11-06 12:44:59 -0800 (Thu, 06 Nov 2003)
Revision: 5076
Log message:

      Need an explicit target for pa_macro.cmi also.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-11-06 16:39:54 -0800 (Thu, 06 Nov 2003)
Revision: 5077
Log message:

      1. Added a theory of nequal:
      'a <> 'b in 'T <--> not{'a='b in 'T}
      
      2. Fix a bug in itt_equal.
      
      3. Add renaming for ordered structure (reverse_order).
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-11-07 02:09:27 -0800 (Fri, 07 Nov 2003)
Revision: 5078
Log message:

      1. Add tactic reduceT = rwAll reduceC.
      
      2. Clean records theories a little bit.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-07 03:07:46 -0800 (Fri, 07 Nov 2003)
Revision: 5079
Log message:

      - Added ".cmoz: .prla .prlb" dependency (with .prl* being optional) and added
      a requirement to build all .cmoz in .DEFAULT. This is necessary to make sure
      that .cmoz is properly updated after .prla is changed (by hand or via CVS).
      
      - Use the new reduceT in existing proofs, where appropriate.
      
      - Fixing itt's OMakefile - Alexei accidentally added the new itt_nequal to
      the PRINT_THEORIES instead of MPFILES.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-11-07 15:03:08 -0800 (Fri, 07 Nov 2003)
Revision: 5080
Log message:

      I fogot to commit the proofs last time. Here they are.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-11-08 16:14:01 -0800 (Sat, 08 Nov 2003)
Revision: 5081
Log message:

      Move the rule for generating rewrite_type_size.mlz before the
      OCamlLibraryInstall so that the copy function will knopw that
      this file can be generated.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-10 15:59:48 -0800 (Mon, 10 Nov 2003)
Revision: 5084
Log message:

      mLast_util.ml now compiles under 3.07. Unfortunately, that is one
      of the easier files, and I still have couple of more compilcated ones
      to update.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-10 18:25:34 -0800 (Mon, 10 Nov 2003)
Revision: 5085
Log message:

      The Filter_hash module needs to go away. A much simpler way
      of location-independent hashing of ML ASTs is by using the
      Reloc module to "relocate" the relevant ASTs to location 0,0
      and to hash the result. This might be somewhat less efficient,
      but we are not planning to use it all that often anyway.
      
      The only thing that prevents me from being able to get rid
      of this module right now is that currenlty only the Pcaml.expr_reloc
      and Pcaml.patt_reloc functions are available, but the other ones
      (str_item_reloc, for example) are not exported. I have filed an RFE
      (see the #1924 at http://caml.inria.fr/bin/caml-bugs/), hopefully
      it will get included in the next release...
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-11 11:52:58 -0800 (Tue, 11 Nov 2003)
Revision: 5086
Log message:

      Use the correct flags when creating .p4 and .p4i
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-11 11:54:38 -0800 (Tue, 11 Nov 2003)
Revision: 5087
Log message:

      Filter compiles under 3.07 now. The next issue to solve is that OCaml complains:
      > The type variable name '_$reduce_resource_annotation is not allowed in programs
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-11 13:14:30 -0800 (Tue, 11 Nov 2003)
Revision: 5088
Log message:

      MetaPRL now compiles with OCaml 3.07
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-11 19:19:52 -0800 (Tue, 11 Nov 2003)
Revision: 5089
Log message:

      Updated the make build subsystem for the 3.07 changes on the branch.
      Note that make will just use "ocamlc -i" to create rewrite_types.mli -
      this is not very efficient, but we should be using omake anyway,
      so it's not too important.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-11 21:34:04 -0800 (Tue, 11 Nov 2003)
Revision: 5090
Log message:

      A few minor clean-ups.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-11 22:06:23 -0800 (Tue, 11 Nov 2003)
Revision: 5091
Log message:

      In "omake realclean", ignore .omakedb, mk/config and mk/config.local
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-12 16:55:59 -0800 (Wed, 12 Nov 2003)
Revision: 5093
Log message:

      Another library file had one of those nasty Not_found-raising gethostname calls,
      bu the result was actually never used, so I deleted the code.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-12 18:37:22 -0800 (Wed, 12 Nov 2003)
Revision: 5095
Log message:

      Fixing bug 116:
      Eliminating another place in Term_ds where nested sequents were not supported.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-12 20:48:57 -0800 (Wed, 12 Nov 2003)
Revision: 5096
Log message:

      Fixing bug 117:
      When turning a sequent into a "generic" term format, the resulting term should
      be destructed right away, not wrapped, otherwise we end up getting an
      infinite loop under Term_std.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-13 10:56:59 -0800 (Thu, 13 Nov 2003)
Revision: 5097
Log message:

      Macro binaries need their $(EXE) suffix on Windows.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-14 13:47:06 -0800 (Fri, 14 Nov 2003)
Revision: 5099
Log message:

      Spelling fixes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-14 16:25:26 -0800 (Fri, 14 Nov 2003)
Revision: 5100
Log message:

      - This is a new approach to handling internal GC in weak_memo - instead
      of relying on OCaml runtime to do the right thing, just count the GC generations
      and include it in the weak descriptors. Note that this change should make the
      3.06 vs 3.07+2 distinction irrelevant.
      
      - This also eliminates the retrieve vs retrieve_hack distinction - now retrieve
      just takes the anchor off the descriptor and it does not require passing the
      whole info as an argument.
      
      Yegor, please take a look when you have time. Thanks!
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-14 17:06:37 -0800 (Fri, 14 Nov 2003)
Revision: 5101
Log message:

      - Be more careful not to GC an entry in the same generation it was created
      - For non-boxed values, set the generation to max_int to make sure that
      it is never GC'ed from the header hash.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-11-14 17:24:28 -0800 (Fri, 14 Nov 2003)
Revision: 5102
Log message:

      Several small updates:
      - Fix a bug in the way how autoT deals with dT n
      - Add a new tactic repeatWithRwsT convs tac - repeatedly apply convs with tac
      - Add some simple rules and definitions (mostly from Nuprl), such as
        hd, tl, all_list, ycomb, nat_plus, outl
      - Add eliminations for atoms equality and product equality.
      
      Question: Do we need eliminations for all equalities?
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-11-15 06:11:03 -0800 (Sat, 15 Nov 2003)
Revision: 5103
Log message:

      Aleksey Nogin wrote:
      
      > Minor thing - why nested if's? This should be just
      >   if (i <= Sequent.hyp_count p) && (alpha_equal t (Sequent.nth_hyp p i))
      >   then raise eq_exn else idT
      
      Yes. I was not sure how && works.
      Fixed.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-11-15 07:45:33 -0800 (Sat, 15 Nov 2003)
Revision: 5104
Log message:

      - Define max and min.
      - Add a small theory itt_fun2 of compose,id,fun_exp. (Stolen from nuprl).
        The theorems in this theory have been proven in Nuprl.
        I'll prove them in Metaprl later.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-11-15 15:54:43 -0800 (Sat, 15 Nov 2003)
Revision: 5105
Log message:

      - natMemberEquality now is intro [AutoMustComplete], not just intro[]
      (because ussually we don't want nat to be destructed automaticly without good reason).
      
      - other small changes
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-11-16 23:46:55 -0800 (Sun, 16 Nov 2003)
Revision: 5106
Log message:

      Fixed some display forms.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-11-17 11:24:43 -0800 (Mon, 17 Nov 2003)
Revision: 5107
Log message:

      Added Mark's theory of messages automata from Nuprl.
      
      Mark and me transfered Nuprl theories (at least basic ones used by message
      automata system) into MetaPRL.
      We did theorems, definitions, and display forms.
      
      mesa/nuprl_* theories are generated from nuprl.
      Some theorems could be stated as better MetaPRL rules.
      we add such theorems in mesa/ma_* theories to avoid conflicts in the case if
      we want to regenerate Nuprl theories.
      
      The dependency is the following:
      Ma_(theory) depends on Nuprl_(theory) and
      Nuprl_(theory) depends on Ma_(previous theory)
      
      
      Eventually all Nuprl stuff should go to appropriate place in Itt.
      (Some stuff is already their).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-17 13:33:19 -0800 (Mon, 17 Nov 2003)
Revision: 5108
Log message:

      The new Alexei's version of the dT-elim autoT-compatibility test turned out
      to be a bit too weak, resulting in autoT going into an infinite loop on occasion.
      Making the test a little stronger.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-17 17:53:09 -0800 (Mon, 17 Nov 2003)
Revision: 5109
Log message:

      - Fixing couple of proofs that were broken by the recent commits.
      - Changed ASCII IO to avoid putting empty space at the end of
      some of the lines in .prla files.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-11-17 21:52:00 -0800 (Mon, 17 Nov 2003)
Revision: 5110
Log message:

      
      Some proofs in mesa theory.
      The proof of
      /nuprl_ring__leader1_object_directory/nuprl_ring__leader1__compatible
      takes 10 minutes in Nuprl and only 5 sec in Metaprl.
      (Measurement was done on differnt machines, but still impressive).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-18 14:40:20 -0800 (Tue, 18 Nov 2003)
Revision: 5111
Log message:

      Camlp4 allows antiquotations in grammar rules; there is no need to use sed...
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-18 21:44:39 -0800 (Tue, 18 Nov 2003)
Revision: 5112
Log message:

      Merged the Exn_boot and Filter_exn modules a bit.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-18 23:55:23 -0800 (Tue, 18 Nov 2003)
Revision: 5113
Log message:

      Print expansion errors using the Filter_exn.print instead of Refine_exn.print.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-19 11:48:50 -0800 (Wed, 19 Nov 2003)
Revision: 5114
Log message:

      This is a no-op commit that removes some white space.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-19 11:50:46 -0800 (Wed, 19 Nov 2003)
Revision: 5115
Log message:

      ******** WARNING - this commit breaks .prlb compatibility ******
      ******** Export all unsaved proofs to .prla before updating ****
      
      - This commit fully implements the "infix" keyword that allows declaring
      infix operators in MetaPRL files (with proper inheritance and scoping).
      We used to have a partial implementation of it, but it did not work and was
      not used.
      
      - I also added the "suffix" keyword that is similar to the "infix" one.
      
      - I changed the implementation of the standard infixes (such as thenT and thenC)
      and the standard suffix (ttca) to use the proper mechanism instead of a filter
      hack that defined all the infixes and suffixes globally as a part of the filter
      code.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-11-19 22:10:54 -0800 (Wed, 19 Nov 2003)
Revision: 5116
Log message:

      Improvement of global GC strategy (though it will probably be replaced with generational GC). Now it's not really global but sticks to mutually recursive memos only.
      I tried different values of threshold in weak_memo.ml but recompilation of metaprl for different values didn't show any substantial difference in compilation time (basically for two settings - often and never).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-20 01:39:18 -0800 (Thu, 20 Nov 2003)
Revision: 5117
Log message:

      Fixing a typo in Yegor's recent commit.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2003-11-21 14:59:22 -0800 (Fri, 21 Nov 2003)
Revision: 5118
Log message:

      Added cross-session readline history support.  Use environment variables
      MP_HISTORY_FILE (default ~/.metaprl_history) and MP_HISTORY_LENGTH (default 100)
      to customize behavior.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-24 16:34:17 -0800 (Mon, 24 Nov 2003)
Revision: 5119
Log message:

      - Do not print a warning message in the Readline history file does not exist.
      
      - Fixed some of the summary dforms (this is a follow-up for
      http://cvs.cs.cornell.edu:12000/commitlogs/metaprl/2003-11.html#03/11/19.14:50:46 )
      
      - Updated the BUGS list a bit.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-11-25 09:21:25 -0800 (Tue, 25 Nov 2003)
Revision: 5120
Log message:

      Update the OMakefile to 0.7.7
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-25 15:55:10 -0800 (Tue, 25 Nov 2003)
Revision: 5121
Log message:

      - (bug 45) in "cvs realclean", skip .omakedb, mk/config and mk/config.local
      - (bug 106) check CAMLLIB, OCAMLLIB and CAMLP4LIB environment variables
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-25 17:12:49 -0800 (Tue, 25 Nov 2003)
Revision: 5122
Log message:

      Go back to the old incremental GC on the trunk. Hopefully, this will allow us
      to collect more data on this crazy bug.
      
      *** Please post to the NG if you see MetaPRL suddenly complaining about PRL ***
      *** contents in a module that you have not changed!!!                       ***
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2003-11-26 11:16:35 -0800 (Wed, 26 Nov 2003)
Revision: 5123
Log message:

      [1] Change one last reference to make to refer to omake.
      [2] Fixed a few typos.
      [3] Added a step/reminder to actually compile OMake if you
          haven't already done so.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-26 15:27:35 -0800 (Wed, 26 Nov 2003)
Revision: 5124
Log message:

      Minor clean-up (removing some unused stuff).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-26 16:21:04 -0800 (Wed, 26 Nov 2003)
Revision: 5125
Log message:

      - Getting rid of the util/misc.ml (ocamldep was barely using it).
      - Allow upper-case file names.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-26 16:56:38 -0800 (Wed, 26 Nov 2003)
Revision: 5126
Log message:

      Actually, it turned out that only 3.07 is capable of dealing with capitalized
      file names, so reverting to only using the lowercase ones.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-26 18:17:01 -0800 (Wed, 26 Nov 2003)
Revision: 5127
Log message:

      This is a no-op commit that removes some white space.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-26 18:19:15 -0800 (Wed, 26 Nov 2003)
Revision: 5128
Log message:

      Use a pa_macro package (loosely based on the pa_macro module from the
      OCaml 3.07 distribution) instead of Eli's macro package.
      
      (This was backported from the ocaml_3_07 branch).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-26 21:41:53 -0800 (Wed, 26 Nov 2003)
Revision: 5129
Log message:

      Omake 0.7.7 still does not do the .mli-free case correctly (see bug 90,
      comments #10 and #11). Chacking in a work-around HACK.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-28 15:27:21 -0800 (Fri, 28 Nov 2003)
Revision: 5130
Log message:

      - Cleaned up some of the MLast.expr handling code (this is backported from
      the ocaml_3_07 branch).
      
      - Updated (with Nathan's help) the text discribing the intro resource annotation
      options, trying to make it a bit more clear.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-30 21:19:52 -0800 (Sun, 30 Nov 2003)
Revision: 5131
Log message:

      (bug 128) Made the Itt_equal.process_eqcd_resource_annotation error messages
      a bit more precise.