Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-03 20:56:02 -0700 (Thu, 03 Jul 2003)
Revision: 87
Log message:

      Beginning the slow process of migrating MetaPRL toward libmojave.
      

Changes by: ( at unknown.email)
Date: 2003-07-03 20:56:02 -0700 (Thu, 03 Jul 2003)
Revision: 88
Log message:

      This commit was manufactured by cvs2svn to create branch
      'abstract_vars'.

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-05 18:25:45 -0700 (Sat, 05 Jul 2003)
Revision: 89
Log message:

      This is partial progress toward abstract vars.  This is a
      branch commit.
      
      I am giving up on this for a moment.  Unfortunately, string
      hacking on variable names is everywhere, not cleanly isolated,
      and not clearly specified.  This makes a port to abstract
      var names either 1) hard, because all this code has to be cleaned
      up, or 2) nonsense, because of the need to covert back and forth
      between strings all the time.
      
      I still think it is a good idea, but it will take a fair amount of
      effort.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-06 16:40:58 -0700 (Sun, 06 Jul 2003)
Revision: 90
Log message:

      I decided to finish the port to abstract vars anyway.
      
      This versdion compiles with omake.  Will fix make next.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-06 19:59:27 -0700 (Sun, 06 Jul 2003)
Revision: 91
Log message:

      Added make support for the abstract vars branch.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-06 21:02:51 -0700 (Sun, 06 Jul 2003)
Revision: 92
Log message:

      It should call itsenf "$DIR", not lm_libmojave.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-06 21:11:13 -0700 (Sun, 06 Jul 2003)
Revision: 93
Log message:

      Migrated String_util and Mp_debug to libmojave versions.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-06 22:48:21 -0700 (Sun, 06 Jul 2003)
Revision: 94
Log message:

      Somehow CVS is ignoring too many files...
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-06 22:53:20 -0700 (Sun, 06 Jul 2003)
Revision: 95
Log message:

      Still recovering from bogus CVS ignored files.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-07 11:00:05 -0700 (Mon, 07 Jul 2003)
Revision: 96
Log message:

      I think this fixes the missing files.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-07 14:42:55 -0700 (Mon, 07 Jul 2003)
Revision: 97
Log message:

      make opt should now work, except on theories/tpt, which is still need
      to fix.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-07 14:57:59 -0700 (Mon, 07 Jul 2003)
Revision: 98
Log message:

      More patches for "make opt"
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-07 16:02:18 -0700 (Mon, 07 Jul 2003)
Revision: 99
Log message:

      <:con< ... >> syntax:
      - for numeric parameters, we can now use syntax $int:expr$, where expr has type int,
      instead of having to convert int to num explicitly.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-07 17:02:55 -0700 (Mon, 07 Jul 2003)
Revision: 100
Log message:

      Moved Array_util to Lm_array_util.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-07 17:07:11 -0700 (Mon, 07 Jul 2003)
Revision: 101
Log message:

      Changed the string representation of variables.  The Lm_symbol.add
      function will now try to parse a numeric suffix correctly.
      The bindings in Filter_util now use strings instead of variables.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-07 18:58:45 -0700 (Mon, 07 Jul 2003)
Revision: 102
Log message:

      - Added Lm-symbol.make that takes an explicit string and an int.
      - The meta-sequent labels are strings, not variables.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-08 18:10:36 -0700 (Tue, 08 Jul 2003)
Revision: 105
Log message:

      This migrates much of the mllib code to libmojave.
      Still to go, use Lm_set instead of Red_black_set,
      but we'll probably do that after we merge onto the trunk.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-08 21:37:34 -0700 (Tue, 08 Jul 2003)
Revision: 106
Log message:

      Lm_symbol.add and Lm_symbol.string_of_symbol now extablish 1-to-1 correspondence
      between symbols and non-empty strings
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-09 00:19:46 -0700 (Wed, 09 Jul 2003)
Revision: 107
Log message:

      Merging in the abstract_vars branch:
      - variables are now an abstract type, not strings
      - MVar parameters are gone
      
      See the branch log messages for more information.
      
      P.S. This is a pretty big change, so I bumped the version number
      in mk/preface.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-09 01:08:27 -0700 (Wed, 09 Jul 2003)
Revision: 108
Log message:

      - Got rid of the LIBMOJAVE parameted in mk/config (just always use $(ROOT)/libmojave)
      - Converted the theories/experimental/compile to be compatible with the current
      incarnation of libmojave
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-11 01:54:00 -0700 (Fri, 11 Jul 2003)
Revision: 110
Log message:

      - Changed the ASCII_IO format to be a bit more flexible. This allowed
      me to get rid of having to print sequents on two separate (hyps and goals) lines.
      For now I had to keep a lot of ugly backwards-compatibility code, but that
      can be cleaned up once we have no files in old format (<= 1.0.6) left.
      
      - Moved the file format version information from Filter_cache to Filter_magic,
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-11 18:54:07 -0700 (Fri, 11 Jul 2003)
Revision: 111
Log message:

      This migrates the set/map code to libmojave.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-12 14:59:12 -0700 (Sat, 12 Jul 2003)
Revision: 112
Log message:

      Migrated more code into libmojave.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-13 03:34:54 -0700 (Sun, 13 Jul 2003)
Revision: 113
Log message:

      Lm_list_util should not inlcude things that already exist in List.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-24 16:10:32 -0700 (Thu, 24 Jul 2003)
Revision: 118
Log message:

      Fixing a recent bug in the "string list list" string parsing code.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-28 11:15:26 -0700 (Mon, 28 Jul 2003)
Revision: 121
Log message:

      Made sure readline C flags are enabled only when READLINE=YES is set.
      

Changes by: ( at unknown.email)
Date: 2003-07-28 11:15:26 -0700 (Mon, 28 Jul 2003)
Revision: 122
Log message:

      This commit was manufactured by cvs2svn to create branch
      'bound_contexts2'.

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-29 20:10:33 -0700 (Tue, 29 Jul 2003)
Revision: 123
Log message:

      Changed itt_logic to use explicit rule calls instead of dT and autoT
      (which can have things overridden in other theories).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-29 22:19:59 -0700 (Tue, 29 Jul 2003)
Revision: 124
Log message:

      I am getting really close on the branch - 1419 out of 1448 proofs
      currently expand correctly.