Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-09-03 12:52:11 -0700 (Sun, 03 Sep 2000)
Revision: 3054
Log message:

      Updated the list of people who contirbuted code to MetaPRL.
      Please take a look and feel free to update your paragraph there.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-09-03 12:55:20 -0700 (Sun, 03 Sep 2000)
Revision: 3055
Log message:

      Fixed links.
      

Changes by: Carl Witty (cwitty at newtonlabs.com)
Date: 2000-09-04 10:09:49 -0700 (Mon, 04 Sep 2000)
Revision: 3056
Log message:

      Started changing declare/prim_rw to define (as in TODO 2.01.2).
      Also fixed an unsoundness in itt_dprod.ml where fst{} had two definitions:
      
       prim_rw unfoldFst : fst{'e} <--> spread{'e; u, v. 'u}
       prim_rw unfoldSnd : fst{'e} <--> spread{'e; u, v. 'v}
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2000-09-10 11:26:37 -0700 (Sun, 10 Sep 2000)
Revision: 3057
Log message:

      This jumbo update is a documentation update.  There are no
      logical changes.  I did two things:
      
      1. First, comments that begin with the sequence "(*!" are
         interpreted as structured comments.  The contents are parsed
         as terms, and the comments will display in the editor window.
         The comments may contain arbitrary text, as usual, and they
         can also contain explicit terms.  The syntax for terms is:
      
         @opname[p1, ..., pn]{t1; ...; tm}
      
         or there is an alternate syntax:
      
         @begin[opname, p1, ..., pn]
         arg
         @end[opname]
      
         Text sequences count as a single term.  So, for instance, the
         term @bf{Hello world} display the "Hello world" text in a bold
         font.
      
         The "doc" term is used for text that is considered to be
         documentation.  There is a set of LaTeX-like terms that you can
         use to produce good-looking documentation.  These are all
         documented in the theories/tactic/comment.ml module.  The exact
         syntax of structured comments is defined in the
         mllib/comment_parse.mll file.  You can also look at any of the
         module in the theories/itt directory if you want to see examples.
      
         You can generate a pritable version of documentation with the
         print_theory command in the editor.  For example, the command
      
         # print_theory "itt_equal";;
      
         produces a file called output.tex that can be formatted with
         your favorite version of latex2e.  You can also generate a
         manule of all the theories by running "make tex" in the
         editor/ml directory.  Or you can run "make" in the
         doc/latex/theories directory.
      
         The files are hyperlinked, and they contain a table of contents
         and an index.  The preferred reader is acrobat, and the preferred
         formatter is pdflatex.
      
      2. Second, I documented the tactic, base, itt, and czf theories.
      
      3. Oh, and I also added a spelling checker:)  You can turn on the
         spelling checker with the -debug spell option or MP_DEBUG=spell.
         If prlc thinks that your files contain spelling mistakes, it will
         print them out and abort.  You can fix this problem by 1) fixing
         the spelling error, 2) adding the words withing a @spelling{words}
         term in a comment, or adding the words to you .ispell_english
         directory.
      
         For example, we could either do this:
      
         @begin[spelling]
         Aleksey Nogin
         @end[spelling]
      
         Or we could just add Alexey to either $cwd/.ispell_english, or
         ~/.ispell_english.
      
         The spell checker uses /usr/dict/words as a database, which it
         compiles to a hashtable in /tmp/metaprl-spell-$USER.dat.  Don't
         worry about the tmp file, it is generated automatically.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2000-09-10 13:41:19 -0700 (Sun, 10 Sep 2000)
Revision: 3058
Log message:

      Last commit failed partway through...
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-09-10 17:31:56 -0700 (Sun, 10 Sep 2000)
Revision: 3059
Log message:

      MetaPRL now requires an extra patch to by applied to Camlp4 -
      Jason's Plexer patch.
      
      The new camlp4 RPM that contains the patch is available at
      ususal places.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2000-09-11 05:58:47 -0700 (Mon, 11 Sep 2000)
Revision: 3060
Log message:

      First compilable version
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2000-09-12 00:56:23 -0700 (Tue, 12 Sep 2000)
Revision: 3061
Log message:

      itt_int_bool_new was split into itt_int_base (beq_int, lt_bool, lt, add, uni_minus, sub, int, ind, number)
      and itt_int_ext (ge_bool, le_bool, gt_bool, ge, le, gt, mul, div, rem)
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2000-09-18 20:03:23 -0700 (Mon, 18 Sep 2000)
Revision: 3062
Log message:

      Sorry, the problem with the last commit was just because of the
      theories/base/base_theory.mlz, which used @begin[tex] instead
      of @begin[doc].  Everything should compile now.
      
      Once it compiles, try using make in the doc/latex/theories
      directory.  It should generate the file all-theories.pdf, which
      is docs for all the modules, including tactics, rules, rewrites,
      etc.  There is an index that you can use to jump to the documentation
      for any particular tactic, etc.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-09-18 22:09:30 -0700 (Mon, 18 Sep 2000)
Revision: 3063
Log message:

      1) "define" currently can't handle recursive difinitions.
      The proper way of doing them is through Y-combinator (a-la-Nuprl),
      but for defining factorial in itt_test, a declare+prim_rw is good enough.
      
      2) Traded "nasty" make warnings for a little less nastier ones.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-09-18 23:36:31 -0700 (Mon, 18 Sep 2000)
Revision: 3064
Log message:

      Documentation Makefiles hacking:
      - Added "texbyte and texopt" in edimor/ml to force using byetcode/native code
      MetaPRL for generating TeX files. "make tex" would use opt if available
      and bytecode otherwise.
      
      - More dependencies to make sure the files are being regenerated as necessary.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2000-09-19 09:46:39 -0700 (Tue, 19 Sep 2000)
Revision: 3065
Log message:

      Fall back to CM fonts in the all-theories.tex file.
      This should fix problem with missing LB (Lucida Bright) fonts.
      My copy of acrobat 4.0 has no trouble reading the result of pdflatex,
      let me know if there are still problems.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-09-19 15:18:30 -0700 (Tue, 19 Sep 2000)
Revision: 3066
Log message:

      - Ocamldep now treats "derive" in the same way as "include" and "open"
      (instead of just ignoring it) which recovered some missing dependencies
      in the FOL theory.
      
      - Better TeX dependencies, including "make tex" now noticing when
      a theory changes.
      
      - Section hack - now Index and Bibliography are created as normal section
      (without two separate "Index" headings as it used to be).
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2000-09-20 15:30:03 -0700 (Wed, 20 Sep 2000)
Revision: 3067
Log message:

      1) Added a new theory (itt_disect) about dependent intersection.
      
      2) Fixed rules intersectionElimination and intersectionSubtype in itt_isect
      
      3) Added a correct version of  intersectionMemberFormation
      
      4) Fixed some comments
      
      5) Added a new bug (4.10) in BUGS
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-09-21 14:18:56 -0700 (Thu, 21 Sep 2000)
Revision: 3068
Log message:

      - Added ~ and sqeq to parser. For now, they produce Perv!"rewrite" terms,
      but once the new rewriting mechanisms are implemented, we'll be able to
      change them to produce "sqeq" opname in "local" theory. I also changed all
      ITT conditional rewrites from Perv!"rewrite" to ~.
      
      - "make clean" now cleans all the new stuff Jason added to doc/{ps,latex}
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-09-21 16:36:46 -0700 (Thu, 21 Sep 2000)
Revision: 3069
Log message:

      Removed some duplicated code.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-09-21 22:24:40 -0700 (Thu, 21 Sep 2000)
Revision: 3070
Log message:

      JProver updates:
      - proper exception handling
      - nicely formatted code
      - a few speed improvements (I just changed a few random things, I have't yet
      looked at speed issues systematically)
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2000-09-22 20:47:08 -0700 (Fri, 22 Sep 2000)
Revision: 3071
Log message:

      I split the Itt_set theory into Itt_hide and Itt_set.
      Note that now the term hide declared in Itt_hide theory, not in Itt_set.
      Let me know if you have problems with this.
      
      Now hide(A) is a full-fledged type.
      We can use it not only for hiding hypothesis,
      but also anywhere in a sequent.
      
      By definition hide(A) is empty if A is empty and has only one
      element "it" otherwise.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-09-23 09:55:53 -0700 (Sat, 23 Sep 2000)
Revision: 3072
Log message:

      Bob's "Agatha" puzzle.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-09-23 13:50:23 -0700 (Sat, 23 Sep 2000)
Revision: 3073
Log message:

      Some of the functions were not wrapped in print_exn for some reason - fixed.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2000-09-23 17:46:18 -0700 (Sat, 23 Sep 2000)
Revision: 3074
Log message:

      Update Itt_logic/implies_df to a nested dform (so it displays recursive
      implications correctly).  Also, fixed a bug in rformat.ml that was causing
      the formatter to calculate the left margin correctly.
      
      I also forgot to mention two new things earlier.  I added the
      cbreak [s1:s; s2:s] display form, which adds a break if the next text
      element would overlow the right margin.  This is useful in text formatting.
      The s1 and s2 are optional; cbreak <--> cbreak[""; " "].  Also, there
      is now a display form pushm[str:s], which adds the text in every
      indentatio, rather than whitespace.  This is useful for comment formatting,
      where the comment lines are indented with the " * " string.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2000-09-23 18:32:28 -0700 (Sat, 23 Sep 2000)
Revision: 3075
Log message:

      Added terminal resizing as Alexey suggested.
      Note that emacs does not use terminals in a shell window...
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2000-09-23 18:42:22 -0700 (Sat, 23 Sep 2000)
Revision: 3076
Log message:

      Oops, that last checkin had a bug: I forgot about the correct
      ordering of fields in a union.  There are separate numbering orders
      for constants and for fields with values.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-09-25 17:09:12 -0700 (Mon, 25 Sep 2000)
Revision: 3079
Log message:

      The result of MP toploop expression evaluation is now also formatted
      using the terminal width. Also, tuples and lists should be now formatted nicer
      in toploop.