Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-10-07 21:25:59 -0700 (Tue, 07 Oct 2003)
Revision: 4955
Log message:

      The very first attempt of rational numbers axiomatization. Some axioms are incorrect.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-10-08 20:07:21 -0700 (Wed, 08 Oct 2003)
Revision: 4957
Log message:

      Minor update
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-10-08 21:30:09 -0700 (Wed, 08 Oct 2003)
Revision: 4958
Log message:

      Complicated pattern in LHS of define beq_rat caused a runtime error. Switched to declare+rewrite.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-09 19:15:07 -0700 (Thu, 09 Oct 2003)
Revision: 4962
Log message:

      Made the error message mentioned in bug 77 a bit more verbose.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-10 17:23:29 -0700 (Fri, 10 Oct 2003)
Revision: 4963
Log message:

      We should always use the proper boolean tests, not $equal(... , YES) ones!
      Hopefully, this will also fix the bug 58.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-10 17:32:40 -0700 (Fri, 10 Oct 2003)
Revision: 4964
Log message:

      Added compile-time checking of definitions (bug 72).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-10-10 19:28:11 -0700 (Fri, 10 Oct 2003)
Revision: 4965
Log message:

      Added the editor/ml/make_mp_version.ml program to *generate* the mp_version.ml
      file.  This works, and it may give us extra flexibility in printing the version
      string.  However, other solutions that work on win32 and Unix are welcome.
      
      WARNING WARNING WARNING: the Weak module in weak_memo.ml is now enabled.
      This hides the weak memo bug, so if you are working on it, be sure to
      change the module name to something else.  However, let's leave it like
      this in the meantime.  It makes running MetaPRL easier, especially on
      win32.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-10-10 19:30:21 -0700 (Fri, 10 Oct 2003)
Revision: 4966
Log message:

      Accidentally disabled the progress bar.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-10-10 19:50:41 -0700 (Fri, 10 Oct 2003)
Revision: 4967
Log message:

      emember the generated .o file.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-10-10 19:54:18 -0700 (Fri, 10 Oct 2003)
Revision: 4968
Log message:

      Ignore some more files.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-10-10 19:56:27 -0700 (Fri, 10 Oct 2003)
Revision: 4969
Log message:

      This file keeps reappearing!
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-10-10 20:39:38 -0700 (Fri, 10 Oct 2003)
Revision: 4970
Log message:

      Short description of itt_int_base, itt_int_ext and itt_int_arith added.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-10-11 08:53:19 -0700 (Sat, 11 Oct 2003)
Revision: 4971
Log message:

      This is a better way to fix the \ vs / problem.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-10-11 09:35:06 -0700 (Sat, 11 Oct 2003)
Revision: 4972
Log message:

      Install prlc into bin/
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-10-11 10:48:19 -0700 (Sat, 11 Oct 2003)
Revision: 4973
Log message:

      Generate .ppo files.
      
      This adds a new section of rules to the toplevel OMakefile.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-10-11 11:26:46 -0700 (Sat, 11 Oct 2003)
Revision: 4974
Log message:

      Add a rule to compile make_mp_version directly, so remove the .mli file.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-10-11 11:31:57 -0700 (Sat, 11 Oct 2003)
Revision: 4975
Log message:

      Remove .ppo, .p4i, and .p4o files during clean.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-10-11 14:23:50 -0700 (Sat, 11 Oct 2003)
Revision: 4976
Log message:

      Fixed the dependencies for mp_version.ml.  Before, it depended on the byte-code
      libraries, causing byte-code to be built even if BYTE_ENABLED=false.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-10-11 22:49:04 -0700 (Sat, 11 Oct 2003)
Revision: 4977
Log message:

      Adding support for document formatting.
      
      For omake, the new style is to add a dcoumentation command in the
      theory, for example, theories/base/OMakefile contains the following:
      
          #
          # Documentation
          #
          PRINT_THEORIES =\
              base_theory\
              top_tacticals\
              top_conversionals\
              var\
              auto_tactic\
              dtactic\
              base_trivial\
              base_rewrite\
              summary\
              comment\
              mptop
      
          TheoryDocument(base, $(PRINT_THEORIES))
      
      I still need to get all-theories right, I'll work on it.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-10-12 01:49:02 -0700 (Sun, 12 Oct 2003)
Revision: 4978
Log message:

      Added all the documentation printers.
      To generate documentation, run the command "omake tex".
      This places the documentation in doc/ps/theories.
      
      This is a new style of documentation: the documentation command
      is in the same OMakefile as the theory itself.  It isn't any
      longer placed in doc/latex/theories; this directory is depracated.
      
      You will need the latest omake to build.  I just added the LaTeX
      generation code.  Also, it only works on Unix for now.
      
      I haven't done the part about generating documentation for all the
      theories at once.  I'll do that tomorrow.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-10-12 12:07:00 -0700 (Sun, 12 Oct 2003)
Revision: 4979
Log message:

      Finished the TeX formatting.
      
      The doc/latex/theories directory is alive again, just for all-theories;
      all the other subdirectories are no longer used.
      
      To make TeX documentation, run "omake tex".  As usual, you can do this
      in the theory subdirectory if you like, and it will just build the
      documentation for that theory.
      
      One issue, the all-theories only builds documentation for the theories
      that are included in THEORIES.  Perhaps we should print a warning in
      this case.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-10-12 13:01:38 -0700 (Sun, 12 Oct 2003)
Revision: 4980
Log message:

      Improved clean.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-10-12 18:36:05 -0700 (Sun, 12 Oct 2003)
Revision: 4981
Log message:

      Add an export line after OMakeFlags(...)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-13 02:23:36 -0700 (Mon, 13 Oct 2003)
Revision: 4982
Log message:

      - Fixing the TESTS=YES compilation (again).
      - make_mp_version needs a ./ path on Unix.
      - No need to clean the tests directory twice.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-13 13:59:56 -0700 (Mon, 13 Oct 2003)
Revision: 4983
Log message:

      Ported the new style of mp_version.ml creating back to make system.
      Now make works again.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-10-13 20:32:57 -0700 (Mon, 13 Oct 2003)
Revision: 4984
Log message:

      Split locale functions from Lm_string_util into Lm_ctype.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-10-13 21:29:40 -0700 (Mon, 13 Oct 2003)
Revision: 4985
Log message:

      Win32 *really* does not like commands that start with ./ or .\.
      For example, ./make_mp_config and .\make_mp_config both do not work.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-10-13 21:30:40 -0700 (Mon, 13 Oct 2003)
Revision: 4986
Log message:

      I should name these variables better.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-14 00:42:44 -0700 (Tue, 14 Oct 2003)
Revision: 4987
Log message:

      Now MetaPRL considers first-order variables to be something entirely seperate
      from second-order ones (even 0-arity ones). Only in special functions
      is_fso_var_term and dest_fso_var, FO variables and 0-arity SO variables
      are not distinguished, but those functions are almost never used.
      
      This fixes bug 75.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-10-14 12:25:45 -0700 (Tue, 14 Oct 2003)
Revision: 4991
Log message:

      Added a version checker to OMakefile.  Sorry, you will have to upgrade
      omake to get this to work, but this will help keep omake and MetaPRL in
      sync.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-15 15:01:21 -0700 (Wed, 15 Oct 2003)
Revision: 4993
Log message:

      - When .omakedb is present, use omake instead of make for check-status.
      - Adding itt_rat to make (already was in omake).
      - Fixing "make clean" in theories/base (I accidentally broke it recently).
      - Removing a weird .camlinit that was there from the beginning of time.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-15 15:39:53 -0700 (Wed, 15 Oct 2003)
Revision: 4994
Log message:

      Make the defaults a bit more explicit.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-15 15:57:34 -0700 (Wed, 15 Oct 2003)
Revision: 4995
Log message:

      Renaming config (make/omake) variables:
      
      TESTS -> TESTS_ENABLED
      READLINE -> READLINE_ENABLED
      NCURSES -> NCURSES_ENABLED
      
      - This makes things more consistent internally
      (all the boolean flags are now called *_ENABLED)
      - This makes things more consistent with how mcc calls them (and we
      want to be able to use MetaPRL's libmojave, which is now the "master" one,
      in mcc).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-15 16:05:41 -0700 (Wed, 15 Oct 2003)
Revision: 4996
Log message:

      Adding a link to Bugzilla (now that we use it so extensively, it needs
      to be up there).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-15 17:06:07 -0700 (Wed, 15 Oct 2003)
Revision: 4998
Log message:

      Gave libmojave its own install target $(LMINSTALL) instead of using
      the common $(MPINSTALL) one.
      
      This is a small step towards making libmojave completely independent (bug 83).
      

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2003-10-15 17:17:36 -0700 (Wed, 15 Oct 2003)
Revision: 4999
Log message:

      added some info about me
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-15 20:23:27 -0700 (Wed, 15 Oct 2003)
Revision: 5000
Log message:

      Moved the core "special" opnames into the Opname module. They used to be
      defined separately in Term module of each of the Refiner implementation,
      but a lot would probably break if different refiners would define these
      opnames differently.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-15 21:21:13 -0700 (Wed, 15 Oct 2003)
Revision: 5001
Log message:

      Working on bug 76. Fixed a number of bugs in Term_std.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-16 20:29:16 -0700 (Thu, 16 Oct 2003)
Revision: 5002
Log message:

      Added two new deug_* variables:
      - debug_full_terms : Print terms fully in debug messages
      - debug_rules: Display rule applications
      
      Refreshed the list of the debug variables in the Developer Guide.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-19 20:17:22 -0700 (Sun, 19 Oct 2003)
Revision: 5003
Log message:

      This fixes a number of bugs in Term_std.
      
      Now bug 76 is almost done - the only differences in proof status
      bewteen Term_std and Term_ds are:
      
      ---
      ds:  Status: /core_type_check/fun_equal is a derived object with an incomplete proof (1 rule boxes, 69 primitive steps)
      std: Status: /core_type_check/fun_equal is a derived object with a complete proof (1 rule boxes, 76 primitive steps)
      
      ds:  Status: /itt_cyclic_group/subg_isCyclic is a derived object with a complete proof (35 rule boxes, 18230 primitive steps)
      std: Status: /itt_cyclic_group/subg_isCyclic is a derived object with a complete proof (35 rule boxes, 18298 primitive steps)
      
      ds:  Status: /itt_nat/int_div_rem is a derived object with a complete proof (51 rule boxes, 129005 primitive steps)
      std: Status: /itt_nat/int_div_rem is a derived object with a complete proof (51 rule boxes, 128785 primitive steps)
      
      ds:  Status: /itt_nat/positive_rule1 is a derived object with a complete proof (38 rule boxes, 70360 primitive steps)
      std: Status: /itt_nat/positive_rule1 is a derived object with an incomplete proof (38 rule boxes, 71208 primitive steps)
      ---
      
      The /core_type_check/fun_equal one is a part of bug 95 (hard to figure out
      until the blocking bug 94 is fixed).
      
      Hopefully, Yegor would have some idea on what is going on in /itt_nat/positive_rule1.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-10-19 21:38:37 -0700 (Sun, 19 Oct 2003)
Revision: 5004
Log message:

      Updated ...partially...! to the new omake build.
      This just does the OMakeroot change.
      I'll commit a change soon for optional dependencies.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-10-19 21:45:14 -0700 (Sun, 19 Oct 2003)
Revision: 5005
Log message:

      Add the optional dependencies.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-10-19 22:15:36 -0700 (Sun, 19 Oct 2003)
Revision: 5006
Log message:

      Ouch!  I'm sorry, the build fails on mojave!
      
      I tested on dual-proc RH9 at home, but apparently there
      is different behavior on mojave.  Please don't use omake version
      0.7.1 until I figure this out...
      
      I don't have time tonight, but I'll check asap...
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-20 15:50:21 -0700 (Mon, 20 Oct 2003)
Revision: 5009
Log message:

      Adding full bibliography data for the MetaPRL TPHOLs 2003 system description.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-20 15:57:08 -0700 (Mon, 20 Oct 2003)
Revision: 5010
Log message:

      Somehow this was dropped from the file, adding back.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-10-20 20:37:07 -0700 (Mon, 20 Oct 2003)
Revision: 5011
Log message:

      Force the use of omake 0.7.1, with optional dependencies.
      
      This addresses bug #59: omake does no rescan a .ml file when a .mli file
      is added.  Not closing the ticket, I have to verify it fixes the problem.
      
      A few minor changes cleaning up OMakefiles in theories/mojave.
      
      !!! Sorry, I cried wolf !!!  The new version of omake works just fine
      on mojave.  Uh, well, it happens I was checked out on the mojave_sequents
      branch on mojave, and of course that version is broken.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-20 22:43:16 -0700 (Mon, 20 Oct 2003)
Revision: 5012
Log message:

      Adding the theories/mojave/arch/ra directory to the make build system.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-20 23:21:12 -0700 (Mon, 20 Oct 2003)
Revision: 5014
Log message:

      The .cmx: .cmx dependencies were not generated correctly in case of .mlz files.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-20 23:24:58 -0700 (Mon, 20 Oct 2003)
Revision: 5015
Log message:

      Killing a number of unneeded 'open' directives.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-10-21 11:52:05 -0700 (Tue, 21 Oct 2003)
Revision: 5016
Log message:

      Started the Mojave compiler paper for the FDL.  The intro must be changed.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-10-21 11:52:51 -0700 (Tue, 21 Oct 2003)
Revision: 5017
Log message:

      Ignore fdl generated files.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-10-21 11:53:44 -0700 (Tue, 21 Oct 2003)
Revision: 5018
Log message:

      Remember to clean up generated files.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-10-21 13:04:51 -0700 (Tue, 21 Oct 2003)
Revision: 5019
Log message:

      Initial FDL version of the M-paper.
      
      A reminder, to build it, cd to the expiremental/compile
      directory, and run "omake tex", or "omake m-paper-fdl.ps"
      for example.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-21 16:14:27 -0700 (Tue, 21 Oct 2003)
Revision: 5022
Log message:

      Removed the optional .mli dependencies from the .SCANNER rules.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-21 21:58:47 -0700 (Tue, 21 Oct 2003)
Revision: 5023
Log message:

      Moving shell_http to support/shell, where it belongs.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-21 22:52:30 -0700 (Tue, 21 Oct 2003)
Revision: 5024
Log message:

      This fixes bug 87: now MetaPRL will use Lm_terminfo instead of using
      hardcoded strings for TERM=xterm only.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-10-22 09:35:42 -0700 (Wed, 22 Oct 2003)
Revision: 5025
Log message:

      Add squashed-dependencies.  This requires the use of omake 0.7.2.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-22 13:17:33 -0700 (Wed, 22 Oct 2003)
Revision: 5026
Log message:

      Scanner for .ppo also depends on $(squashed-dependencies %.mli)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-22 19:00:34 -0700 (Wed, 22 Oct 2003)
Revision: 5027
Log message:

      OCaml version is in mk/defaults now, not mk/preface.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-22 19:37:58 -0700 (Wed, 22 Oct 2003)
Revision: 5028
Log message:

      Explicitly point to the README file in the patches directory.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-10-22 20:32:27 -0700 (Wed, 22 Oct 2003)
Revision: 5029
Log message:

      Added a new intro to the FDL paper.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-22 20:35:14 -0700 (Wed, 22 Oct 2003)
Revision: 5030
Log message:

      - Adding a "doc" target that would build all the files that are
      currently posted on the web (note: some of the "omake tex" files
      require Lucida fonts, but "omake doc" should work without them).
      
      - Added htmldoc html->ps/pdf converter to omake and added the
      htmldoc-generated files to "omake doc"
      
      - make will now print a warning message telling people that
      using make is no longer recommended and that omake should
      be used instead.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-10-23 12:07:47 -0700 (Thu, 23 Oct 2003)
Revision: 5032
Log message:

      Build the ocaml book from book2.tex.
      This addresses problem 2 in bug #57.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-10-23 12:08:36 -0700 (Thu, 23 Oct 2003)
Revision: 5033
Log message:

      Ignore more generated files.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-23 12:36:43 -0700 (Thu, 23 Oct 2003)
Revision: 5034
Log message:

      "omake doc" include doc/ps/theories/{theories,ocaml-book}.{ps,pdf}
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-23 19:24:37 -0700 (Thu, 23 Oct 2003)
Revision: 5035
Log message:

      - This fixes all-theories.pdf build (bug 57)
      
      - In bytecode mode, omake should use mp.top, not mp.opt
      
      - Made ocamldep -prl mode a bit smarter:
      a) When a PRL .mli file contains "mptop", then .cmi dependes on Shell_sig and Mptop
      modules
      b) When a PRL file contains "interactive", "interactive_rw" or "derived", then it
      depeneds on the Shell module
      c) All PRL .cmx and .cmo files depend on Shell_sig and Mptop signatures (strictly speaking,
      this is only true when the corresponding .mli contains an "mptop" directive), but this is an
      approximation
      
      - Printexn.catch is a bad idea now (the runtime now is as good at printing uncaught
      exceptions and Printexn.catch blocks exception backtracing), got rid of all of them.
      
      - Print a better error message when trying to cd into a theory that does not exist.
      
      - The all-theories theory list was missing the base_theory file, and the fol_theory one
      should not be there.
      
      - Minor changes in module (AKA theory, AKA package) management in shell.
      
      - Made "omake clean" in editor/ml a bit cleaner
      

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2003-10-24 13:38:19 -0700 (Fri, 24 Oct 2003)
Revision: 5036
Log message:

      Added the ISSRE03 paper on Building reliable compilers using MetaPRL
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-24 16:34:43 -0700 (Fri, 24 Oct 2003)
Revision: 5037
Log message:

      Rewrote the term comparison function. Now the code is cleaner and faster.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-24 17:25:43 -0700 (Fri, 24 Oct 2003)
Revision: 5038
Log message:

      Some more clean-up.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-27 18:22:29 -0800 (Mon, 27 Oct 2003)
Revision: 5039
Log message:

      I rolled back a bunch of changes that were made when reformatting from
      the ACM style to LNCS style, bringing the M paper back to the ACM style.
      
      Hopefully, I rolled back all the right ones (e.g only the formatting ones, but
      not the textual or style fixing ones). I also rolled back most of the changes
      that cut some of the text out, but some of them seemed reasonable regardless
      of space constraints, so I kept the removed text out.
      
      Still need to fix a bunch of overflows.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-27 19:36:11 -0800 (Mon, 27 Oct 2003)
Revision: 5040
Log message:

      Fixed most of the overfulls, other formatting fixes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-28 01:01:10 -0800 (Tue, 28 Oct 2003)
Revision: 5041
Log message:

      Use the same ocaml flags in make, omake and prlc compilations.
      
      Check for pa_op.cmo/cmx in addition to camlp4.cma/cmxa (in OCaml 3.07
      camlp4.cmxa is there by default, but pa_op.cmx is not :-( ).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-28 01:09:39 -0800 (Tue, 28 Oct 2003)
Revision: 5042
Log message:

      In the previous commit I undated the checks, but forgot to update the error
      messages.
      

Changes by: ( at unknown.email)
Date: 2003-10-28 01:09:39 -0800 (Tue, 28 Oct 2003)
Revision: 5043
Log message:

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

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-28 01:56:43 -0800 (Tue, 28 Oct 2003)
Revision: 5044
Log message:

      First step towards making it work with OCaml 3.07 (on a branch for now).
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-10-28 16:14:59 -0800 (Tue, 28 Oct 2003)
Revision: 5045
Log message:

      Two debug variables debug_graph_arith1 and debug_graph_arith2 added.
      When first of them set to true, /itt_nat/positive_rule1/1/2/3 become incomplete for Term_ds in the same way as for Term_std with same unproved inequality 0+m>=(1+m)+-1+y.
      The only thing that happens when you set debug_graph_arith1 to true is several calls to TermMan.nth_hyp. Any comments?
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-28 21:37:36 -0800 (Tue, 28 Oct 2003)
Revision: 5046
Log message:

      Package.is_loaded used to return "true" for theories that were only partially
      loaded. Eliminating that function.
      
      P.S. The package/theory management need to be cleaned up (a lot), but for now
      I just need something that works.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-28 21:52:20 -0800 (Tue, 28 Oct 2003)
Revision: 5047
Log message:

      Added a few comments.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-28 22:28:40 -0800 (Tue, 28 Oct 2003)
Revision: 5048
Log message:

      A little more progress towards ocaml 3.07 compatibility.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-29 06:35:37 -0800 (Wed, 29 Oct 2003)
Revision: 5049
Log message:

      Working on switching from our ad-hoc macro.ml package to the new pa_macro
      that is included in the distribution. Currently, we need an improved version
      of pa_macro (I with submit these improvements back to OCaml team, of course),
      so for now we need to have a local copy of pa_macro.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2003-10-29 07:24:58 -0800 (Wed, 29 Oct 2003)
Revision: 5050
Log message:

      Fixed a few bugs in the procedure and added info about OMake.  Note that I can't
      reproduce any of the problems Brian had anymore.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-29 07:46:22 -0800 (Wed, 29 Oct 2003)
Revision: 5051
Log message:

      Working on the macro conversion, but omake is giving me trouble.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-29 14:04:22 -0800 (Wed, 29 Oct 2003)
Revision: 5052
Log message:

      Allow more then one macro declaration in branches of an IFDEF.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-29 14:49:48 -0800 (Wed, 29 Oct 2003)
Revision: 5053
Log message:

      Support INCLUDE directives.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-29 15:12:47 -0800 (Wed, 29 Oct 2003)
Revision: 5054
Log message:

      Finished getting rid of rewrite_types_sig module (we had an .mlz file
      generated using the maro package from an .ml file - this was way too messy).
      
      We still need to make sure omake and make would do the right thing since
      we now have a file with .ml, but without a .mli!
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-29 17:35:21 -0800 (Wed, 29 Oct 2003)
Revision: 5055
Log message:

      Implemented SEQ_SET as an actual module, not a macro (the module itself
      still uses macros to figure out which implementation to use).
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-10-29 21:15:06 -0800 (Wed, 29 Oct 2003)
Revision: 5056
Log message:

      Got rid of nth_hyp. Sorry about that - it was a temporary shortcut but became permanent (as usual).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-30 16:28:27 -0800 (Thu, 30 Oct 2003)
Revision: 5057
Log message:

      Added support for   DEFINE name = expr IN expr   "local" macros.
      
      Also made sure local macros and macro params are expanded in "try .. with .."
      expressions.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-30 17:02:24 -0800 (Thu, 30 Oct 2003)
Revision: 5058
Log message:

      Do macro param/local macro substitutions in "do { ... }"
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-10-30 20:06:32 -0800 (Thu, 30 Oct 2003)
Revision: 5059
Log message:

      After all I was looking in the wring place. The problem fixed by replacing progressT with repeatT in Itt_int_arith.sumListT. It looks like progressT behaves differently in Term_std (from Term_ds).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-30 21:42:09 -0800 (Thu, 30 Oct 2003)
Revision: 5060
Log message:

      Implemented the "NOTHING" macro.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-30 23:47:20 -0800 (Thu, 30 Oct 2003)
Revision: 5061
Log message:

      Refiner finally compiles with the new macro package.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-31 00:06:32 -0800 (Fri, 31 Oct 2003)
Revision: 5062
Log message:

      Better comment.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-31 13:57:08 -0800 (Fri, 31 Oct 2003)
Revision: 5063
Log message:

      Currently, refiner/refsig/*Makefile assume that all files in refiner/refsig
      are .mlz. Therefore, I had to move the new SEQ_SET into refbase.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-31 17:30:23 -0800 (Fri, 31 Oct 2003)
Revision: 5064
Log message:

      Posted the latest version of the MERLIN paper.