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  Path
Added metaprl/editor/ml/.gdbinit
Properties metaprl/editor/ml/.gdbinit
+6 -12 metaprl/editor/ml/Makefile
+3 -3 metaprl/editor/ml/io_proof.ml
+1 -1 metaprl/editor/ml/nlconfig
+1 -1 metaprl/editor/ml/nlgossip
+5 -6 metaprl/editor/ml/nlopt
+1 -1 metaprl/editor/ml/package_info.ml
+7 -4 metaprl/editor/ml/shell_nl.ml
+1 -0 metaprl/editor/ml/shell_p4.ml
+6 -3 metaprl/ensemble/Makefile
+80 -34 metaprl/ensemble/ensemble_queue.ml
+4 -1 metaprl/ensemble/remote_ensemble.ml
+2 -0 metaprl/ensemble/remote_null.ml
+1 -0 metaprl/ensemble/remote_sig.mlz
+3 -4 metaprl/ensemble/thread_refiner_ens.ml
+2 -0 metaprl/ensemble/thread_refiner_null.ml
+1 -0 metaprl/ensemble/thread_refiner_sig.mlz
+1 -4 metaprl/filter/Makefile
Deleted metaprl/filter/buffer.ml
Deleted metaprl/filter/buffer.mli
+1 -1 metaprl/filter/filter_ast.ml
Added metaprl/filter/filter_buffer.ml
Properties metaprl/filter/filter_buffer.ml
Added metaprl/filter/filter_buffer.mli
Properties metaprl/filter/filter_buffer.mli
+1 -1 metaprl/filter/filter_cache_fun.ml
+10 -9 metaprl/filter/filter_comment.ml
+1 -0 metaprl/filter/filter_magic.ml
+3 -1 metaprl/filter/filter_main.ml
+10 -10 metaprl/filter/filter_ocaml.ml
+1 -1 metaprl/filter/filter_ocaml.mli
+1 -1 metaprl/filter/filter_parse.ml
+8 -8 metaprl/filter/filter_prog.ml
+5 -5 metaprl/filter/filter_summary.ml
+1 -1 metaprl/filter/filter_summary_util.ml
+5 -5 metaprl/filter/term_grammar.ml
+1 -3 metaprl/library/Makefile
+1 -1 metaprl/library/ascii_scan.ml
+1 -1 metaprl/library/ascii_scan.mli
+9 -9 metaprl/library/basic.ml
+1 -1 metaprl/library/basic.mli
+11 -10 metaprl/library/db.ml
+0 -1 metaprl/library/library_eval.ml
+2 -2 metaprl/library/link.ml
+7 -7 metaprl/library/mathBus.ml
+1 -1 metaprl/library/mathBus.mli
+2 -1 metaprl/library/mbterm.ml
+4 -4 metaprl/library/nuprl5.ml
+1 -1 metaprl/library/nuprl5.mli
+2 -2 metaprl/library/orb.ml
+1 -0 metaprl/library/registry.ml
+3 -0 metaprl/mllib/Makefile
+1 -0 metaprl/mllib/file_type_base.ml
+1 -0 metaprl/mllib/file_util.ml
Added metaprl/mllib/nl_big_int.ml
Properties metaprl/mllib/nl_big_int.ml
Added metaprl/mllib/nl_big_int.mli
Properties metaprl/mllib/nl_big_int.mli
Added metaprl/mllib/nl_num.ml
Properties metaprl/mllib/nl_num.ml
Added metaprl/mllib/nl_num.mli
Properties metaprl/mllib/nl_num.mli
Added metaprl/mllib/nl_pervasives.ml
Properties metaprl/mllib/nl_pervasives.ml
Added metaprl/mllib/nl_pervasives.mli
Properties metaprl/mllib/nl_pervasives.mli
+2 -0 metaprl/mllib/remote_lazy_queue.ml
+3 -1 metaprl/mllib/remote_lazy_queue_sig.ml
+3 -0 metaprl/mllib/remote_queue_null.ml
+11 -2 metaprl/mllib/remote_queue_sig.ml
+1 -1 metaprl/refiner/reflib/Files
+1 -1 metaprl/refiner/reflib/ml_format_sig.mlz
+1 -1 metaprl/refiner/reflib/ml_print.ml
Added metaprl/refiner/reflib/nl_resource.ml
Properties metaprl/refiner/reflib/nl_resource.ml
Added metaprl/refiner/reflib/nl_resource.mli
Properties metaprl/refiner/reflib/nl_resource.mli
Deleted metaprl/refiner/reflib/resource.ml
Deleted metaprl/refiner/reflib/resource.mli
+1 -1 metaprl/refiner/reflib/rformat.ml
+1 -1 metaprl/refiner/reflib/rformat.mli
+1 -1 metaprl/refiner/reflib/term_copy.ml
+6 -6 metaprl/refiner/refsig/term_op_sig.ml
+1 -1 metaprl/refiner/refsig/term_simple_sig.mlz
+1 -1 metaprl/refiner/rewrite/rewrite.mlp
+9 -9 metaprl/refiner/rewrite/rewrite_build_contractum.mlp
+2 -2 metaprl/refiner/rewrite/rewrite_debug.mlp
+1 -1 metaprl/refiner/rewrite/rewrite_match_redex.mlp
+2 -2 metaprl/refiner/rewrite/rewrite_type.mlp
+2 -2 metaprl/refiner/rewrite/rewrite_type_sig.mlz
+1 -1 metaprl/refiner/term_ds/term_ds.ml
+1 -1 metaprl/refiner/term_ds/term_ds_sig.ml
+1 -1 metaprl/refiner/term_ds/term_subst_ds.mlp
+1 -1 metaprl/refiner/term_std/term_std.ml
+1 -1 metaprl/refiner/term_std/term_std_sig.ml
+1 -1 metaprl/refiner/term_std/term_subst_std.mlp
+1 -1 metaprl/theories/base/base_auto_tactic.ml
+1 -1 metaprl/theories/base/base_auto_tactic.mli
+1 -1 metaprl/theories/base/base_cache.ml
+1 -1 metaprl/theories/base/base_dtactic.ml
+1 -1 metaprl/theories/base/base_rewrite.ml
+1 -1 metaprl/theories/base/typeinf.ml
+1 -1 metaprl/theories/czf/czf_itt_all.ml
+1 -1 metaprl/theories/czf/czf_itt_and.ml
+1 -1 metaprl/theories/czf/czf_itt_dall.ml
+1 -1 metaprl/theories/czf/czf_itt_dexists.ml
+1 -1 metaprl/theories/czf/czf_itt_empty.ml
+1 -1 metaprl/theories/czf/czf_itt_eq.ml
+1 -1 metaprl/theories/czf/czf_itt_eq_inner.ml
+1 -1 metaprl/theories/czf/czf_itt_exists.ml
+1 -1 metaprl/theories/czf/czf_itt_false.ml
+1 -1 metaprl/theories/czf/czf_itt_implies.ml
+1 -1 metaprl/theories/czf/czf_itt_member.ml
+1 -1 metaprl/theories/czf/czf_itt_or.ml
+1 -1 metaprl/theories/czf/czf_itt_pre_set.ml
+1 -1 metaprl/theories/czf/czf_itt_rel.ml
+1 -1 metaprl/theories/czf/czf_itt_sall.ml
+1 -1 metaprl/theories/czf/czf_itt_sep.ml
+1 -1 metaprl/theories/czf/czf_itt_set.ml
+1 -1 metaprl/theories/czf/czf_itt_set_ext.ml
+1 -1 metaprl/theories/czf/czf_itt_set_ind.ml
+1 -1 metaprl/theories/czf/czf_itt_sexists.ml
+1 -1 metaprl/theories/czf/czf_itt_small.ml
+1 -1 metaprl/theories/czf/czf_itt_true.ml
+1 -1 metaprl/theories/czf/czf_itt_union.ml
+9 -9 metaprl/theories/itt/itt_arith.ml
+1 -1 metaprl/theories/itt/itt_atom.ml
+1 -1 metaprl/theories/itt/itt_bool.ml
+1 -1 metaprl/theories/itt/itt_derive.ml
+1 -1 metaprl/theories/itt/itt_dfun.ml
+1 -1 metaprl/theories/itt/itt_dprod.ml
+1 -1 metaprl/theories/itt/itt_equal.ml
+1 -1 metaprl/theories/itt/itt_fun.ml
+1 -1 metaprl/theories/itt/itt_int.ml
+2 -2 metaprl/theories/itt/itt_int.mli
+1 -1 metaprl/theories/itt/itt_isect.ml
+1 -1 metaprl/theories/itt/itt_list.ml
+1 -1 metaprl/theories/itt/itt_logic.ml
+1 -1 metaprl/theories/itt/itt_prec.ml
+1 -1 metaprl/theories/itt/itt_prod.ml
+1 -1 metaprl/theories/itt/itt_quotient.ml
+1 -1 metaprl/theories/itt/itt_rfun.ml
+1 -1 metaprl/theories/itt/itt_set.ml
+1 -1 metaprl/theories/itt/itt_squash.ml
+1 -1 metaprl/theories/itt/itt_srec.ml
+1 -1 metaprl/theories/itt/itt_struct.ml
+1 -1 metaprl/theories/itt/itt_subtype.ml
+1 -1 metaprl/theories/itt/itt_test.ml
+1 -1 metaprl/theories/itt/itt_union.ml
+1 -1 metaprl/theories/itt/itt_unit.ml
+1 -1 metaprl/theories/itt/itt_void.ml
+1 -1 metaprl/theories/itt/itt_w.ml
+1 -1 metaprl/theories/tactic/nltop.ml
+1 -0 metaprl/theories/tactic/tactic_type.ml
+1 -0 metaprl/theories/tactic/tactic_type.mli
+1 -1 metaprl/theories/tptp/tptp.ml
+1 -0 metaprl/theories/tptp/tptp_load.ml
+6 -1 metaprl/theories/tptp/tptp_prove.ml
+1 -1 metaprl/util/ocamldep.mll