Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-08-02 10:12:26 -0700 (Sun, 02 Aug 1998)
Revision: 2380
Log message:

      Modified rewriter to handle Alexey's new sequents.  The rewriter is
      now moved to a new directory refiner/rewrite.  Clause numbers in
      TermMan now start with 1.  The tactics seem to work, but there may
      be some lurking problems with hypothesis numbering.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-02 10:45:16 -0700 (Sun, 02 Aug 1998)
Revision: 2381
Log message:

      Fixed some dependencies
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-08-02 12:24:58 -0700 (Sun, 02 Aug 1998)
Revision: 2382
Log message:

      Added performance testing function.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-08-02 12:43:20 -0700 (Sun, 02 Aug 1998)
Revision: 2383
Log message:

      Updated z.ml for testing.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-02 12:57:06 -0700 (Sun, 02 Aug 1998)
Revision: 2384
Log message:

      Bigger example
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-02 13:23:43 -0700 (Sun, 02 Aug 1998)
Revision: 2385
Log message:

      Added the bound variables occurs check to the unification
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-02 13:48:09 -0700 (Sun, 02 Aug 1998)
Revision: 2386
Log message:

      Added editor/ml directory to the profiled build
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-02 13:58:11 -0700 (Sun, 02 Aug 1998)
Revision: 2387
Log message:

      Pass all $(OCAMLOPTFLAGS) to ocamlopt when building nl.opt
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-08-02 14:36:26 -0700 (Sun, 02 Aug 1998)
Revision: 2388
Log message:

      Added #quit directive, and interactive_flag to reduce output in
      non-interactive sessions.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-08-02 14:37:47 -0700 (Sun, 02 Aug 1998)
Revision: 2389
Log message:

      There is some thread problem preventing exiting; override the exit with
      and explicit call to _exit(code).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-08-02 14:38:16 -0700 (Sun, 02 Aug 1998)
Revision: 2390
Log message:

      Flush output in time_it().
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-08-02 16:38:49 -0700 (Sun, 02 Aug 1998)
Revision: 2391
Log message:

      Added splay_tables, which act like functional hash tables over
      an ordered type.  This code is derived from Splay_set.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-02 18:17:09 -0700 (Sun, 02 Aug 1998)
Revision: 2392
Log message:

      Made splay code faster by decreasing its memory usage
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-08-02 18:55:50 -0700 (Sun, 02 Aug 1998)
Revision: 2393
Log message:

      Added a append function to the SplayTable.union function so that
      duplicate entries can be removed when the tables are merged.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-02 20:13:54 -0700 (Sun, 02 Aug 1998)
Revision: 2394
Log message:

      Pass $(PROFILE) flag to gcc
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-02 20:14:38 -0700 (Sun, 02 Aug 1998)
Revision: 2395
Log message:

      Call write_profiling() before exiting
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-02 20:47:59 -0700 (Sun, 02 Aug 1998)
Revision: 2396
Log message:

      It is $(ROOT), not $(REF_ROOT)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-02 22:02:42 -0700 (Sun, 02 Aug 1998)
Revision: 2397
Log message:

      Faster splay code
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-03 05:55:18 -0700 (Mon, 03 Aug 1998)
Revision: 2398
Log message:

      Fixed profiling build
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-08-03 11:32:42 -0700 (Mon, 03 Aug 1998)
Revision: 2399
Log message:

      Splay_table is now thread-safe, and mostly functional.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-08-03 18:34:48 -0700 (Mon, 03 Aug 1998)
Revision: 2400
Log message:

      Added Splay_table caching in TPTP.
      Fixed choice of rotate_left_right and rotate_right_left
      in Splay_table.lift.
      timingT tactic now reports the timing correctly.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-08-04 09:49:19 -0700 (Tue, 04 Aug 1998)
Revision: 2401
Log message:

      Added somewhat functional splay sets.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-08-04 12:33:52 -0700 (Tue, 04 Aug 1998)
Revision: 2402
Log message:

      Relaxed addressing to allow rewriting in hyp Contexts.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-04 14:38:57 -0700 (Tue, 04 Aug 1998)
Revision: 2403
Log message:

      Putting size only in Node, not in Leaf saves some memory
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-08-04 16:46:32 -0700 (Tue, 04 Aug 1998)
Revision: 2404
Log message:

      Fixed a problem with Fun_splay_set.union, which was introducing
      non-sorted splay trees.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-04 16:59:31 -0700 (Tue, 04 Aug 1998)
Revision: 2405
Log message:

      Script to run nl.top
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-08-04 17:00:04 -0700 (Tue, 04 Aug 1998)
Revision: 2406
Log message:

      Tptp_cache is using fun_splay_set.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-08-04 18:12:22 -0700 (Tue, 04 Aug 1998)
Revision: 2407
Log message:

      Added util String_set module.
      Unification now used String_set.StringSet for the constants (Term_ds
      still uses its own StringSet).
      Modified sequent display.
      Added Shell.goal () to the the current proof goal.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-04 20:22:01 -0700 (Tue, 04 Aug 1998)
Revision: 2408
Log message:

      A useful tool for debugging new implementations of Set module
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-04 20:57:18 -0700 (Tue, 04 Aug 1998)
Revision: 2409
Log message:

      Inlining rotate_* functions "by hands" saves some memory allocations
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-04 21:16:46 -0700 (Tue, 04 Aug 1998)
Revision: 2410
Log message:

      When v is not in s, "remove v s" should return s, not a copy of s.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-05 11:37:10 -0700 (Wed, 05 Aug 1998)
Revision: 2411
Log message:

      Compute the free variables lazily
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-08-05 18:52:46 -0700 (Wed, 05 Aug 1998)
Revision: 2412
Log message:

      Fixed unification to compare constants after bound variables,
      and to unify constants like other terms.  Fixed a problem with
      bound variable naming in hypothesis rewriting.  TPTP quantifiers
      are over atom0.
      
      Finally, terms that are equal may not be alpha-equal.  Never assume
      that ordinary equality (=) on terms has any logical meaning.  Fixed
      equality bug on xnil_term in TermMan.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-06 09:09:27 -0700 (Thu, 06 Aug 1998)
Revision: 2413
Log message:

      In add function, when element is already there,
      update the tree according to th result of the splay operation
      before returning
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-06 11:09:44 -0700 (Thu, 06 Aug 1998)
Revision: 2414
Log message:

      Splay_table: fixed some bugs and did some optimizations
      Tptp_prove: loopTestT: changed the number of calls to proveT from 100 to 200
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-06 14:00:55 -0700 (Thu, 06 Aug 1998)
Revision: 2415
Log message:

      Faster term camparison
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-06 14:29:07 -0700 (Thu, 06 Aug 1998)
Revision: 2416
Log message:

      Removed some unused code (set_of_list function)
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-08-06 15:11:58 -0700 (Thu, 06 Aug 1998)
Revision: 2417
Log message:

      Yet another fix to unification.  Changes have not been added to
      term_std.  There is a problem with delayed free_var computation
      in term_ds.  Patched it temporarily.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-06 15:27:36 -0700 (Thu, 06 Aug 1998)
Revision: 2418
Log message:

      Using Small_set version (with max_length=12) makes things faster
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-06 16:55:51 -0700 (Thu, 06 Aug 1998)
Revision: 2419
Log message:

      Check if the substitution is non-empty before calling do_term_subst
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-08-06 18:48:31 -0700 (Thu, 06 Aug 1998)
Revision: 2420
Log message:

      Added unify_subst type to retain unification info between separate
      calls to TermSubst.unify.  This requires that type inference be modified,
      and there are still some small modifications to be made in Itt_rfun.
      We need to do some optimization in Cycle_dag and unification.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-06 20:48:49 -0700 (Thu, 06 Aug 1998)
Revision: 2421
Log message:

      Removed "ugly" sequents.
      Term_base_ds: now dest_term will raise Invalid_argument
                    when called on a sequent term
      Simple_print: I wrote some temporary code for printing sequents,
                    but it should definitely be rewritten
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-06 21:55:24 -0700 (Thu, 06 Aug 1998)
Revision: 2422
Log message:

      Fixed some functions that were calling dest_term on sequents
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-07 17:35:17 -0700 (Fri, 07 Aug 1998)
Revision: 2423
Log message:

      Fixed a bug with wrong delayed variable calculation in delayed substitution
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-07 18:01:25 -0700 (Fri, 07 Aug 1998)
Revision: 2424
Log message:

      Moved the check for empty substitution into the rewriter
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-08 09:31:35 -0700 (Sat, 08 Aug 1998)
Revision: 2425
Log message:

      Made variables (including so-variables) a "special" term.
      Removed extra (term) argument from dest_simple_bterm function
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-08 11:47:15 -0700 (Sat, 08 Aug 1998)
Revision: 2426
Log message:

      It seems better to have a separate "special" form for FO-vars.
      Right now SO vars are kept in "ugly" form,
      but we may create a new "special" form for them later.
      
      Important: mk_so_var v [] creates an "ugly" 0-ary SO var which is different
      from FO var: it has no free variables and is not recognized by is_var_term
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-08 12:21:11 -0700 (Sat, 08 Aug 1998)
Revision: 2427
Log message:

      Faster dest_term, is_var_term and dest_var functions
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-08 13:26:00 -0700 (Sat, 08 Aug 1998)
Revision: 2428
Log message:

      Eliminated some calls to dest_term on FO vars
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-08 13:33:47 -0700 (Sat, 08 Aug 1998)
Revision: 2429
Log message:

      Fixed a typo
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-08 14:54:32 -0700 (Sat, 08 Aug 1998)
Revision: 2430
Log message:

      Eliminated some closure creation
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-08 16:15:17 -0700 (Sat, 08 Aug 1998)
Revision: 2431
Log message:

      Cleaner a little faster code for unification.
      I added some bvars checking and marked a place
      where we should add a full bound variable occurs check
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-08 16:51:12 -0700 (Sat, 08 Aug 1998)
Revision: 2432
Log message:

      Removed unused mk_var_op function
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-08-10 10:19:03 -0700 (Mon, 10 Aug 1998)
Revision: 2433
Log message:

      Added red-black set implementation.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-10 10:27:31 -0700 (Mon, 10 Aug 1998)
Revision: 2434
Log message:

      Added some (hopefully) useful information from my letter to V.N.Krupski
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-10 11:01:28 -0700 (Mon, 10 Aug 1998)
Revision: 2435
Log message:

      Since Fun_splay_set in much faster than Splay_set
      and Red_black_set is even faster, there is no reason
      to keep Splay_set
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-10 11:14:53 -0700 (Mon, 10 Aug 1998)
Revision: 2436
Log message:

      We used to have S (Set) module signature defined in Splay_set.
      Now I added a new file for that.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-08-10 17:44:46 -0700 (Mon, 10 Aug 1998)
Revision: 2437
Log message:

      Red_black_set.union inserts the smaller tree into the larger,
      which is a little faster than flattening the trees.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1998-08-13 08:58:24 -0700 (Thu, 13 Aug 1998)
Revision: 2438
Log message:

      Removed redundant onSomeHyp from base_auto_tactic.
      Added proveInt in test.ml.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1998-08-13 13:26:48 -0700 (Thu, 13 Aug 1998)
Revision: 2439
Log message:

      Placed propDecideT in itt_prop_decide.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-08-17 08:28:26 -0700 (Mon, 17 Aug 1998)
Revision: 2440
Log message:

      Added multithreaded refinement.  NOTE: this requires a patch to
      LinuxThreads.  The patched library is in clib/libpthreads-i386-linux.lib.
      I'll add the source level patch in the next release.
      
      Removed failure caching from tptp_prove to get more deterministic
      refinements.  Modified Tptp_prove.testT to create a single proof
      goal, rather than running proveT several times.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1998-08-17 19:31:31 -0700 (Mon, 17 Aug 1998)
Revision: 2441
Log message:

      Changed the `directory' separator from "." to "/";
      cd changes info.dir only after possible errors.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-08-21 15:22:55 -0700 (Fri, 21 Aug 1998)
Revision: 2442
Log message:

      Added distributed refinement using Ensemble.
      This is an initial version.  The scheduler needs some performance
      tuning, and Ensemble needs a little work on blocking IO.
      
      By default, Ensemble support is not compiled into Nuprl-Light.
      To enable distributed refinement, you need a copy of Ensemble,
      which is available at:
      
          http://www.cs.cornell.edu/Info/Projects/Ensemble/
      
      When Ensemble is installed, set the environment variable
      ENSROOT to the root Ensemble directory.  On mojave, I've precompiled
      a version of Ensemble in ~jyh/nuprl/src/ensemble.  Once this
      variable is set, make will build the distributed refiner.
      
      Ensemble uses a separate "gossip" daemon to get processes to form groups.
      The program editor/ml/nlgossip starts this daemon.  Once the daemon
      is started, multiple copies of nl will know about each other, and ship
      refinement jobs to each other.  So if you want faster refinement, start
      multiple copies of nl.  These copies can be started and killed at
      any time; Ensemble provides support for failure detection and recovery.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-08-24 06:43:48 -0700 (Mon, 24 Aug 1998)
Revision: 2443
Log message:

      Slightly better Ensemble scheduling.
      Native-code compiler has trouble marshaling functions--
      its probably a problem with the marshaler.
      
      Added Nl_num, a ML-only implementation of bignums.
      This is slower than the C version used by OCaml, but
      we can marshal the Nl_nums.  Most of the files changed
      are just replacements of Num.* with Nl_num.*.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-24 14:30:03 -0700 (Mon, 24 Aug 1998)
Revision: 2444
Log message:

      Added captions
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-24 15:00:10 -0700 (Mon, 24 Aug 1998)
Revision: 2445
Log message:

      Added some comments on how the free_vars and bfree_vars fields in the Term_ds
      term types are being computed.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-24 15:27:19 -0700 (Mon, 24 Aug 1998)
Revision: 2446
Log message:

      Added "exists x . (x = y)" example.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-24 15:48:50 -0700 (Mon, 24 Aug 1998)
Revision: 2447
Log message:

      They are SOVar's, not TVar's.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-24 16:01:16 -0700 (Mon, 24 Aug 1998)
Revision: 2448
Log message:

      Added the HTML'ized Term_ds type definitions.
      Based on the file written by V.Krupski.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1998-08-24 17:09:49 -0700 (Mon, 24 Aug 1998)
Revision: 2449
Log message:

      Fixed a small bug in compare_param, and changed indentation.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1998-08-25 14:26:33 -0700 (Tue, 25 Aug 1998)
Revision: 2450
Log message:

      Some more indentations.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-26 22:11:39 -0700 (Wed, 26 Aug 1998)
Revision: 2451
Log message:

      When building it optimized without Ensemble, do not forget to link .a file
      to the lib dir.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-08-27 06:45:19 -0700 (Thu, 27 Aug 1998)
Revision: 2452
Log message:

      Fixed the thread problem without Ensemble.  Removed the library
      temporarily until files can be upgraded to OCaml 2.0.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-29 11:46:42 -0700 (Sat, 29 Aug 1998)
Revision: 2453
Log message:

      Removed all references to "/usr/local/lib/nuprl-light" from the code