Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-05-03 05:11:21 -0700 (Mon, 03 May 1999)
Revision: 2649
Log message:

      Added an initial incomplete version of the distributed marshaler.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 1999-05-03 11:40:52 -0700 (Mon, 03 May 1999)
Revision: 2650
Log message:

      Alexei & Alexey:
      Fixed some small typos in the documentation noticed by Alexei Kopylov.
      
      In partucular, interactive_rw was misspelled as interactiverw and
      the documentation was still referring to d_resource.improve_resource instead
      of Mp_resource.resource_improve
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-05-04 08:34:58 -0700 (Tue, 04 May 1999)
Revision: 2651
Log message:

      Fixed a type error in define_axiom.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 1999-05-13 16:18:29 -0700 (Thu, 13 May 1999)
Revision: 2652
Log message:

      1) Added a bug list into BUGS
      
      2) Changed the keywords:
      axiom -> rule  (.mli files)
      primrw -> prim_rw  (.ml files)
      rwthm -> thm_rw  (.ml files)
      
      3) Fixed the rule Itt_struct.hypSubstitution
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-05-16 13:49:56 -0700 (Sun, 16 May 1999)
Revision: 2653
Log message:

      Added: MetaPRL toploop does not produce any meaningful parsing errors
      
      Fixed spelling.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 1999-05-16 14:05:14 -0700 (Sun, 16 May 1999)
Revision: 2654
Log message:

      Added: loading two theories that both include the same theory produces unexpected results
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-05-17 12:20:58 -0700 (Mon, 17 May 1999)
Revision: 2655
Log message:

      Added pthreads instructions
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-05-19 14:08:40 -0700 (Wed, 19 May 1999)
Revision: 2656
Log message:

      The rule for induction on W-types was unsound.  Fix thanks
      to Carl Witty <cwitty@newtonlabs.com>.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-05-20 13:45:26 -0700 (Thu, 20 May 1999)
Revision: 2657
Log message:

      Make sure OCAMLSRC and ENSROOT are non-empty
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-05-20 14:27:59 -0700 (Thu, 20 May 1999)
Revision: 2658
Log message:

      Added the Refiner information (VERBOSE/SIMPLE and ds/std) into mp_version
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-05-20 16:03:12 -0700 (Thu, 20 May 1999)
Revision: 2659
Log message:

      - Fixed a bug in Term_ds:
      The code responsible for renaming bound variables was lost during code reorganization in the
      revision 1.34 of term_base_ds.mlp on 1998/12/30
      
      - Fixed a bug in Term_ds and Term_std:
      Functon match_terms never checked if the matched term on the right-hand side had any
      improperly bound variables. As a result,
      match_terms [] <<lambda{y.('f 'y)}>> <<lambda{x.('x 'x)}>>
      was returning
      Refiner.Refiner.TermSubst.term_subst = ["f", x]
      instead of raising an exception
      
      - Some file headers still had "This file is part of Nuprl-Light" instead of
      "This file is part of MetaPRL" - fixed
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 1999-05-20 16:11:57 -0700 (Thu, 20 May 1999)
Revision: 2660
Log message:

      Fixed fun_df3:
      
       dform fun_df3 : rfun{'A; f, x. 'B['f; 'x]} =
      -   "{" " " slot{bvar{'f}} `"|" "fun"{'A; x. 'B['f; 'x]} "}"
      +   "{" " " slot{bvar{'f}} `" | "  slot{bvar{'x}} `":" slot{'A} " " rightarrow " " slot{'B} "}"
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-05-20 18:22:28 -0700 (Thu, 20 May 1999)
Revision: 2661
Log message:

      - Updated the BUGS file
      
      Changes suggested by Carl R. Witty <cwitty@newtonlabs.com>:
      - Give better error message when $(OSTYPE) is unknown
      - Added comments to mk/config telling that the file is generated
      

Changes by: ( at unknown.email)
Date: 1999-05-20 18:22:28 -0700 (Thu, 20 May 1999)
Revision: 2662
Log message:

      This commit was manufactured by cvs2svn to create tag
      'meta-prl-0_5_2'.

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-05-20 18:37:22 -0700 (Thu, 20 May 1999)
Revision: 2663
Log message:

      I tagged the current version with meta-prl-0_5_2 tag and bumped the version number
      to 0.5.3
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-05-21 12:03:44 -0700 (Fri, 21 May 1999)
Revision: 2664
Log message:

      Added MPPATH environment variable (as requested by Mark Bickford)
      for specifying an include path for prlc.  Directories are separated by :,
      and -I <dir> command line arguments will append to this path.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 1999-05-21 16:34:22 -0700 (Fri, 21 May 1999)
Revision: 2665
Log message:

      Added: cd theory;; load theory;; <<it>> produces an error
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-05-21 18:28:28 -0700 (Fri, 21 May 1999)
Revision: 2666
Log message:

      I hope I've fixed the OSTYPE/pthreads check.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-05-22 04:24:29 -0700 (Sat, 22 May 1999)
Revision: 2667
Log message:

      Modified the itt_rfun display form to be recursive.
      Sorry about the delay.  I forgot, and cs-annex-1 is
      having trouble.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-05-22 17:00:51 -0700 (Sat, 22 May 1999)
Revision: 2668
Log message:

      Added ML side-conditions, so that rewrites and rules can be defined
      with ML code in the really necessary cases.  The ml_rw keyword
      declares/defines an ML rewrite, and ml_rule declares/defines
      an rule application defined in ML.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-05-23 14:55:17 -0700 (Sun, 23 May 1999)
Revision: 2669
Log message:

      This is a major modification to how parameters are handled.
      1. All level parmeters are now meta.  That is, univ[@i:l] is
         exactly the same as univ[i:l].  The rewriter handles
         lavel expressions, so matching with levels like
         univ[3 | i':l | j:l] should work correctly.
      
         The syntax still requires the @ for meta-parameter of
         other types.  For instance, token["hello world":t] is
         a normal token, and token[@"hello world":t] is a
         token with a meta-parameter.
      
      2. There are no more parameter expressions.  For instance,
         the term natural_number[@i + @j] is not valid anymore.
         To replace them, the module theories/base/base_meta.ml
         defines ML rewrites that implement the same functionality.
         For example,
            meta_sum{number[12]; number[5]} --> number[17]
      
      3. There is no term natural_number[@i:n] any more.  This was
         always a bad name, since it has always been possible for the
         parameter to be negative.
      
      4. The Itt_equal.cumulativity rule is no longer defined as a
         side-condition.  It now uses Base_meta.meta_lt to define
         inclusion on level expression.  Cumulativity expansion
         should be performed automatically by the dT tactic.
         So:
            sequent ['ext] { ... >- univ[@i:l] = univ[@i:l] in univ[@j:l] }
            BY dT 0
         should always either succeed or fail, without producing
         subgoals.
      
      I haven't fully tested the side-conditions.  As usual, let me know
      if you see anything strange.  Next, I'm looking at the
      rewriter free variable soundness problem.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-05-23 15:38:46 -0700 (Sun, 23 May 1999)
Revision: 2670
Log message:

      TermSubst.equal_params should be called recursively when argument is a ParamList
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-05-24 19:12:01 -0700 (Mon, 24 May 1999)
Revision: 2671
Log message:

      OK, here is the updated code for the weak-pointers based Term_copy modules
      
      The changes include:
      1) I added the new garbage collecting mechanism written by Yegor.
      2) Parameters are now hashed as a whole instead of recursively weak-hashing them.
      3) I merged the TermHeader module into the TermHash module which allowed me to keep
         most TermHash types abstract.
      4) I cleaned up the code a little.
      
      Yegor, can you run some test on this code and see if there is any evidence that we
      still have the bug? Thanks!
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-05-25 13:20:28 -0700 (Tue, 25 May 1999)
Revision: 2672
Log message:

      I hope I have fixed the problem with .prlb files
      that Alexei was having.  This is a real HACK!  We'll
      want to remove all code marked HACK! when we save
      formatted proofs.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-05-25 13:28:16 -0700 (Tue, 25 May 1999)
Revision: 2673
Log message:

      .
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-05-25 17:41:08 -0700 (Tue, 25 May 1999)
Revision: 2674
Log message:

      I removed @ from the parameter syntax for meta-parameters. Now
      [xxx:s] is parsed as a meta-string parameter (MString "xxx") and
      ["xxx":s] is parsed as a string parameter (Sting "xxx")
      
      I also copied .cmoz files to .prlb files until I've reached a fixpoint.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-05-26 23:24:53 -0700 (Wed, 26 May 1999)
Revision: 2675
Log message:

      Added *.ppo.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-05-27 00:55:33 -0700 (Thu, 27 May 1999)
Revision: 2676
Log message:

      Changed X' identifiers to X1 to avoid the preprocessor problem with the
      newer gcc and added a comment in the TODO file to restore this once the ML
      preprocessor is working.  Also, removed the *.ppo from the .cvsignore - I
      didn't realize that this problem left the .ppo file...
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-05-27 05:31:06 -0700 (Thu, 27 May 1999)
Revision: 2677
Log message:

      Fix some slot[lt]{...} and slot[le]{...} to use quotes.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-05-27 06:44:24 -0700 (Thu, 27 May 1999)
Revision: 2678
Log message:

      Reworked some parts so now it works fine again.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-05-27 09:43:35 -0700 (Thu, 27 May 1999)
Revision: 2679
Log message:

      Few more minor fixes.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-05-30 15:00:34 -0700 (Sun, 30 May 1999)
Revision: 2680
Log message:

      In Itt_list.nilFormation, 'A list should be list{'A}.
      Thanks to Carl Witty <cwitty@newtonlabs.com>.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-05-31 22:47:13 -0700 (Mon, 31 May 1999)
Revision: 2681
Log message:

      - Fixed a nasty bug in TermAddr.apply_var_fun_higher_bterms (both ds and std versions).
      Thanks to Carl R. Witty <cwitty@newtonlabs.com> for finding and fixing this one.
      
      - Added a warning to mp-install.html telling that MetaPRL is Beta and still has nasty bugs.
      
      - Added CVS read-write instructions:
      http://ensemble01.cs.cornell.edu:12000/cvsweb/~checkout~/meta-prl/doc/htmlman/mp-cvs-rw.html