Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-04-01 02:05:14 -0800 (Tue, 01 Apr 2003)
Revision: 4362
Log message:

       - Proved "Every subgroup of a cyclic group is cyclic" with Alexei's membership for subset.
       - A slight change in the definition of subStructure.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-01 14:17:43 -0800 (Tue, 01 Apr 2003)
Revision: 4363
Log message:

      Added the SPEC file.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-04-01 16:11:11 -0800 (Tue, 01 Apr 2003)
Revision: 4364
Log message:

      Changed well-formedness rules.
      Added a squash-stable rule for subStructure with squash resource.
      
      Can anyone, maybe Aleksey, please take a look at "itt_grouplikeobj/subStructure_sqStable1"? I can't figure out how to prove it. Thanks.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-04-01 16:23:17 -0800 (Tue, 01 Apr 2003)
Revision: 4365
Log message:

      Simplified some proofs.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-04-01 16:42:44 -0800 (Tue, 01 Apr 2003)
Revision: 4366
Log message:

      Removed "subStructure_sqStable1".
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-01 18:31:14 -0800 (Tue, 01 Apr 2003)
Revision: 4367
Log message:

      Updated the squash resource to support annotations on
      H |- [A] --> H |- A
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-01 21:49:19 -0800 (Tue, 01 Apr 2003)
Revision: 4368
Log message:

      Use -lncurses (which exists on UGCS machines) instead of -ltermcap (which does not).
      

Changes by: ( at unknown.email)
Date: 2003-04-01 22:26:24 -0800 (Tue, 01 Apr 2003)
Revision: 4369
Log message:

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

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-01 22:26:24 -0800 (Tue, 01 Apr 2003)
Revision: 4370
Log message:

      CS101-specific version string.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-04-02 02:29:52 -0800 (Wed, 02 Apr 2003)
Revision: 4372
Log message:

      Completed all proofs except for "itt_subset/member_doesnot_depend_on_B".
      
      Alexei, can you take a look at this rule? I think the assumptions should
      be subset instead of subtype.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-04-02 15:53:40 -0800 (Wed, 02 Apr 2003)
Revision: 4373
Log message:

      1.itt_logic/not_elim had incorrect label of the only subgoal (assert->main).
      2.negation and nequal in hypotheses are supported now.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2003-04-02 16:12:23 -0800 (Wed, 02 Apr 2003)
Revision: 4374
Log message:

      These are bug fixes so that the M language compiler can be built
      again.  Someone mispelled 'cmxa' in editor/ml/Makefile.  Also, the
      list of files was incorrect in compile/Makefile.  Finally, there
      was an unused match case in M_x86_term (how it managed to survive
      this long is beyond me).
      
      Incidentally, it would appear that in order to build the M
      language compiler, lm_libmojave has to be a subdirectory of
      MetaPRL?  At least that's the only way I could get it to work.
      
      One last thing, only an 'opt' build seems to work if all I have
      is  THEORIES = tactic ocaml base experimental/compile.  A
      byte-code build keeps dying in editor/ml becuase it seems like
      lm_libmojave/cutil never gets built (and I don't know why).
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2003-04-02 22:42:22 -0800 (Wed, 02 Apr 2003)
Revision: 4375
Log message:

      Wrote a little documentation for dead code elimination.  Mostly,
      this is just clean-up.  Is 'redeces' the plural form of 'redex'?
      If it isn't, that'll need to be fixed here.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2003-04-03 00:34:13 -0800 (Thu, 03 Apr 2003)
Revision: 4376
Log message:

      This is my attempt to add some saner documentation to M_inline.
      As in M_dead, there's not a whole lot to say.  We need to discuss
      the technical report for the M language compiler sometime.
      
      I believe we have a bug in the rewrite to perform constant folding
      for division operations.  The problem is the reduction of
      meta_quot will fail is we're trying to divide by zero, which means
      that we could potentially end up with a program that has
      extraneous MetaInt terms.
      
      I would fix this using a conditional rewrite (which is the only
      immediately obvious thing that I can think of), except I'm under
      the impression we're trying to avoid conditional rewrites (can't
      remember where I heard this).  In any event, I put a BUG marker on
      the rewrite for now.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-04-03 03:19:38 -0800 (Thu, 03 Apr 2003)
Revision: 4379
Log message:

      Defined subgroup; Updated some proofs. Need to work more on this tomorrow.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2003-04-03 09:36:07 -0800 (Thu, 03 Apr 2003)
Revision: 4380
Log message:

      Tried to clean-up the documentation in M_prog.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2003-04-03 13:03:26 -0800 (Thu, 03 Apr 2003)
Revision: 4381
Log message:

      Removing my BUG comment, given Jason's response to it
      (see the newsgroup).
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2003-04-03 15:56:18 -0800 (Thu, 03 Apr 2003)
Revision: 4382
Log message:

      A little more work on trying to clean-up / add documentation.
      I need to take a look at the assembly language some more; the
      delete_null_reserve rewrite confuses me right now.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2003-04-03 16:14:56 -0800 (Thu, 03 Apr 2003)
Revision: 4383
Log message:

      Added booleans to the abstract syntax table and cleaned up
      trailing whitespace chars.  Not sure how much else I want to
      try cleaning up in this file before we get together to talk
      about the tech report.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2003-04-03 18:28:01 -0800 (Thu, 03 Apr 2003)
Revision: 4384
Log message:

      This will be my final attempt at trying to add/fix documentation
      for a while.  The documentation in M_x86_asm is still lacking in
      places, but I think it's a bit better than what was there before.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-04-04 19:23:14 -0800 (Fri, 04 Apr 2003)
Revision: 4385
Log message:

      More updates on stuff related to subgroup.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-04-05 00:58:44 -0800 (Sat, 05 Apr 2003)
Revision: 4386
Log message:

      Updated proofs related with subgroup.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-04-05 02:39:25 -0800 (Sat, 05 Apr 2003)
Revision: 4387
Log message:

      Changed the definition of cyclic subgroup.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-06 13:29:55 -0700 (Sun, 06 Apr 2003)
Revision: 4388
Log message:

      Fixed the "make latex".
      
      Xin, when writing TeX display forms, the things that can be long and may end up
      broken into several lines should not be wrapped in {...}.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-06 23:20:22 -0700 (Sun, 06 Apr 2003)
Revision: 4389
Log message:

      New syntax for sequent context and binding-free sequent hypotheses.
      
      Note: in "... sequent ...{ <H>..." there now _needs_ to be a space
      between "{" and "<" (I have idea why camlp4 acts this way).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-07 00:07:28 -0700 (Mon, 07 Apr 2003)
Revision: 4390
Log message:

      Updated the display forms for the new sequent syntax.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-07 00:45:04 -0700 (Mon, 07 Apr 2003)
Revision: 4392
Log message:

      - Using the new syntax, got rid of some unused binding vars
      - The rule itt_rfun.well_founded_assum_elim had a wrong "squash" marker.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-07 01:07:36 -0700 (Mon, 07 Apr 2003)
Revision: 4393
Log message:

      Created an empty cs101 theory
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-07 02:26:01 -0700 (Mon, 07 Apr 2003)
Revision: 4394
Log message:

      - Added the basic intuitionistic rules to the cs101 theory
      - Term grammar: hyp variables should be LINDENT's, not just word_or_string's
      - File_base: better error message in the "not found" case.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-07 11:32:07 -0700 (Mon, 07 Apr 2003)
Revision: 4395
Log message:

      - Better (and more insane, of course) grammar for distinquishing between hyp
      bindings and binding-free hyps.
      - xterm scripts will now explicitly use +bdc (display bold as color).
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-04-07 13:02:48 -0700 (Mon, 07 Apr 2003)
Revision: 4396
Log message:

      1.itt_bool - removed incorrect rule that I added earlier
      2.itt_int_base - cleaning, all proofs are completed.
      3.itt_int_ext - some proofs completed.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-07 17:10:39 -0700 (Mon, 07 Apr 2003)
Revision: 4397
Log message:

      Proofs from today's lecture.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-07 18:14:30 -0700 (Mon, 07 Apr 2003)
Revision: 4398
Log message:

      Made it more robust.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-07 18:25:20 -0700 (Mon, 07 Apr 2003)
Revision: 4399
Log message:

      Furthe font selector script fixes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-07 21:03:45 -0700 (Mon, 07 Apr 2003)
Revision: 4401
Log message:

      Do not try cleaning the directories that do not exist.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-07 22:11:38 -0700 (Mon, 07 Apr 2003)
Revision: 4402
Log message:

      Updating the README (thanks to Michael Vanier for noticing some
      potentially misleading text in it).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-08 16:35:31 -0700 (Tue, 08 Apr 2003)
Revision: 4403
Log message:

      - Added a "raw" display form mode that is _guaranteed_ not to have any display
      forms (unfortunatelly the "src" mode has a lot of stuff that is not supposed
      to be there!). To use, do
      cd "/";; set_dfmode "raw";;
      in toploop.
      - Updated the Simple_print module to use the new syntax for sequents.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-08 18:49:29 -0700 (Tue, 08 Apr 2003)
Revision: 4404
Log message:

      - Now the Pcaml.Qerror exceptions are pretty-printed correctly
      (instead of just being printed in the unexpanded format), so
      the term parsing errors are reported in a human-readable way now.
      - When there is a parsing error, the readline buffer is flushed
      (which means no further error get reported when it attempts to parse
      the ramaining buffer starting at a random point where the previous
      parsing attempt failed).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-08 22:26:42 -0700 (Tue, 08 Apr 2003)
Revision: 4405
Log message:

      CS101: Classical logic and the other part of the homework.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-09 00:30:13 -0700 (Wed, 09 Apr 2003)
Revision: 4406
Log message:

      Comment parsing:
      - now it does not make sence to consider "*" symbol after whitespace
      at the beginning of a new line as a whitespace.
      
      Comment prl display:
      - "@begin[doc]", "@end[doc]", "(*" and "*)" will now be displayed bold
      - Multi-line comment will now be correctly terminated by " *)" on the last line,
      and not " *  *)"
      
      mpxterm scripts:
      - mpxterm will now use the same font for normal and bold display (since the
      bold version of the fond does not have tha "vdash" symbol).
      - both mpxterm and mpxterm-large will now display bold as brown.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-09 18:30:13 -0700 (Wed, 09 Apr 2003)
Revision: 4408
Log message:

      Proof automation from lecture 4.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-10 21:25:37 -0700 (Thu, 10 Apr 2003)
Revision: 4409
Log message:

      Minor clean-up.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-11 00:18:24 -0700 (Fri, 11 Apr 2003)
Revision: 4410
Log message:

      - The "doc" directive now does not require the <:doc< >> quotation. One
      can now use normal terms (applytermlist, to be exact; no quotations required)
      under it.
      
      - <:doc<, <:ext<, << (<:term<) quotations can now be freely mixed (except
      inside <:ext:<, probably - Adam, will non-Phobos quotations be recognized
      correctly inside the Phbos syntax?). Note, that <:doc< >> will produce an
      xlist term with all white space being Comment!comment_write, so is would not
      be a good idea to use those in formal environment. But doing things like
      doc ... <:doc< ... << ... >> .. >> ...
      Should work fine.
      
      - When <:doc< is immediatelly (e.g. on top level) inside the "doc"
      str/sig_item, it will be parsed _delayed_ (e.g. only after the rest of the file
      is processed, including all the declare directives that might go _after_ it.
      Normal terms and <:doc< syntax in other places will be parsed right away.
      
      - The <;doc< and <:ext< quotations are now available in top loop and not just
      in .ml file compilation (Adam, please take a look and see if I did it correcty.
      In particular, is there anything in Phobos that does not need to be compiled in?).
      
      - The qoutations are now handled in term_grammar, not in filter_parse (since
      filter_parse is _not_ a part of top loops, while term_grammar is). This meant
      having to move term_grammar to be _after_ the phobos in the compilation
      order, which meant having to move it to filter/filter.
      
      - Changed ocamldep to ignore module names inside quotations. This helps
      get rid of bogus dependencies for filter_prog (which is full of <:expr< >>
      quotations that have module names in them).
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-04-11 01:02:31 -0700 (Fri, 11 Apr 2003)
Revision: 4411
Log message:

      Defined group isomorphism and did a little adjustment to the def. of group homomorphism.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-04-11 04:10:03 -0700 (Fri, 11 Apr 2003)
Revision: 4412
Log message:

      Defined group kernel.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-11 16:00:48 -0700 (Fri, 11 Apr 2003)
Revision: 4413
Log message:

      Minor updates.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-11 17:00:45 -0700 (Fri, 11 Apr 2003)
Revision: 4414
Log message:

      Updated the dmoz link.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-11 18:01:29 -0700 (Fri, 11 Apr 2003)
Revision: 4415
Log message:

      Declare the rules as tactics.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-11 19:35:17 -0700 (Fri, 11 Apr 2003)
Revision: 4416
Log message:

      Typo fix.
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-04-11 22:57:30 -0700 (Fri, 11 Apr 2003)
Revision: 4417
Log message:

      Added basic skeleton of M techreport. For now, it has the same
      introduction and parsing section as the paper, and the rest
      are the theory files (not all).
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-04-11 23:01:12 -0700 (Fri, 11 Apr 2003)
Revision: 4418
Log message:

      Forgot to add generated files to .cvsignore.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-04-12 03:03:10 -0700 (Sat, 12 Apr 2003)
Revision: 4419
Log message:

      Rule-proving...
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-04-12 03:32:25 -0700 (Sat, 12 Apr 2003)
Revision: 4420
Log message:

      Changed the definition of group kernel.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-04-13 04:44:19 -0700 (Sun, 13 Apr 2003)
Revision: 4421
Log message:

      Redefined normal subgroup with _extensional_ set equality (using "esquash") and proved more properties of the group kernel.
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-04-13 18:52:14 -0700 (Sun, 13 Apr 2003)
Revision: 4422
Log message:

      Generated tex files for M weren't cleaned.
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-04-13 22:40:01 -0700 (Sun, 13 Apr 2003)
Revision: 4423
Log message:

      Added display forms for numbers and basic arithmetic operations.
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-04-13 22:40:35 -0700 (Sun, 13 Apr 2003)
Revision: 4424
Log message:

      Fixed typo in display form.
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-04-14 00:34:35 -0700 (Mon, 14 Apr 2003)
Revision: 4425
Log message:

      Various display form improvements and some of the text in
      the code generation section.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-04-14 00:53:33 -0700 (Mon, 14 Apr 2003)
Revision: 4426
Log message:

      Defined group monomorphism/epimorphism; Changed the definition of group
      isomorphism; And added/proved more properties.
      
      Now everything about groups in CZF is implemented in ITT except the example
      of Klein 4-group.
      
      "groupMono_ker2" remains unproved since it requires some esquash equality
      elimination.
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-04-14 01:03:29 -0700 (Mon, 14 Apr 2003)
Revision: 4427
Log message:

      Better display forms for helper terms.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-14 17:00:55 -0700 (Mon, 14 Apr 2003)
Revision: 4429
Log message:

      - Simplified the libmojave conditionals in Makefile
      - Made "make depend" do the right thing with libmojave
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-04-14 18:03:56 -0700 (Mon, 14 Apr 2003)
Revision: 4430
Log message:

      Changed all occurrences of extensional set equality to use "ext_equal"
      instead of "esquash".
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-14 18:47:36 -0700 (Mon, 14 Apr 2003)
Revision: 4431
Log message:

      Tried to simplify the shell interfaces a little.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-14 21:23:26 -0700 (Mon, 14 Apr 2003)
Revision: 4432
Log message:

      Forgot to clean out.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-04-15 13:48:46 -0700 (Tue, 15 Apr 2003)
Revision: 4433
Log message:

      | Add preliminary omake build system.
      |
      | Here's some things I haven't done yet.
      |    1. Support for some .PHONY targets like "clean".
      |    2. TeX compilation needs support in editor/ml/OMakefile.
      |    3. Haven't tried "omake -j 4" yet.
      |    4. editor/ml/Makefile is pretty ugly, could be cleaned up.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-04-15 13:48:47 -0700 (Tue, 15 Apr 2003)
Revision: 4434
Log message:

      | Add preliminary omake build system.
      |
      | Here's some things I haven't done yet.
      |    1. Support for some .PHONY targets like "clean".
      |    2. TeX compilation needs support in editor/ml/OMakefile.
      |    3. Haven't tried "omake -j 4" yet.
      |    4. editor/ml/Makefile is pretty ugly, could be cleaned up.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-04-15 14:30:04 -0700 (Tue, 15 Apr 2003)
Revision: 4435
Log message:

      Files was accidentally added to lm_libmojave.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-04-15 14:31:59 -0700 (Tue, 15 Apr 2003)
Revision: 4436
Log message:

      File was added on branch lm_libmojave.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-04-15 16:08:51 -0700 (Tue, 15 Apr 2003)
Revision: 4437
Log message:

      Added one group example (integer under addition).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-04-15 18:22:52 -0700 (Tue, 15 Apr 2003)
Revision: 4438
Log message:

      Minor omake changes.
      Problem: ocamldep does not generate dependencies on .mlz files.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-04-15 21:10:47 -0700 (Tue, 15 Apr 2003)
Revision: 4439
Log message:

      Added clean and realclean targets.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-16 00:22:53 -0700 (Wed, 16 Apr 2003)
Revision: 4440
Log message:

      Made a pass of code clean-up in filter_prog.
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-04-16 14:20:19 -0700 (Wed, 16 Apr 2003)
Revision: 4442
Log message:

      Added comments on asm code generation.
      Removed all display forms from the tech report.
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-04-16 15:06:33 -0700 (Wed, 16 Apr 2003)
Revision: 4443
Log message:

      Added new abstract syntax for M.
      Next is to define the AST->IR conversion.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-16 18:37:46 -0700 (Wed, 16 Apr 2003)
Revision: 4444
Log message:

      HW2 solutions.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-16 22:58:54 -0700 (Wed, 16 Apr 2003)
Revision: 4445
Log message:

      Use orelseT in completelyDestructT.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-16 23:21:30 -0700 (Wed, 16 Apr 2003)
Revision: 4446
Log message:

      Hopefully I finally got it right.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-17 18:43:40 -0700 (Thu, 17 Apr 2003)
Revision: 4447
Log message:

      - Instead of always using {\bf ...}, {\it ...}, etc, now @tt uses \texttt{...}
      in text mode and \mathtt{...} in math mode.
      - The comment parser now knows that @mbox and @hbox take you out of math mode.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-17 21:54:21 -0700 (Thu, 17 Apr 2003)
Revision: 4448
Log message:

      Further clean-up.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-17 23:09:20 -0700 (Thu, 17 Apr 2003)
Revision: 4449
Log message:

      - More precise error messages when parsing comments:
      a) The "undeclared opname" errors now give the address of the actual opname,
      not of the whole comment the opname is in
      b) The error messages that happen when parsing a << >> quotation inside
      <:doc< >> quotation now give the actual address, not the address relative to
      the << beginning. These messages currently give the address a few symbols off,
      not sure why.
      
      - The << >> quotations inside <:doc< >> are now always assumed to imply the
      math mode. I.e. <:doc< ... << ... >> ... >> will get parsed the same as
      <:doc< ... $<< ... >>$ ... >> (unless, of course, the << ... >> was already
      inside the math mode).
      
      - Started getting rid of unneeded math_ terms in itt_comment.
      
      - Made the display form for esquash nicer (uses the actual double-bracket
      symbols instead of [[ ]] which can be confused with squash{squash{ }}).
      
      - The display form for assert is up arrow (it used to be inconsistent -
      up in some places, down in some), same as in Nuprl (in Nuprl, the
      downarrow is a display form for squash).
      
      - Fixed the prl mode dform for sube.
      
      - Spelling fixes
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-18 17:54:03 -0700 (Fri, 18 Apr 2003)
Revision: 4454
Log message:

      Reducing dependencies of Filter_prog (I am planning to move it to filter/filter
      and stop compiling it into the editor/ml/mp.* binaries).
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-04-18 19:07:33 -0700 (Fri, 18 Apr 2003)
Revision: 4455
Log message:

      Xin and Aleksey:
      - defined a cong symbol
      - made sure sub<x> is defined (and correctly defined) for all
      "x" from a through z.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-18 21:29:12 -0700 (Fri, 18 Apr 2003)
Revision: 4456
Log message:

      - Moved Filter_prog from filter/base to filter/filter and removed it
      from the list of modules being linked into the editor/ml/mp.* binaries.
      
      - Also, simplified some of the signatures (replacing functors with plain modules)
      
      Note: we might want to be eventually able to define things on-line from the toploop
      and filter_prog might be useful to have linked in for that purpose. But currently
      filter_parse is in filter/filter (and not being linked in anyway), so this change
      does not make things any worse than they already were.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-18 22:13:09 -0700 (Fri, 18 Apr 2003)
Revision: 4457
Log message:

      - Updated the installation instruction
      
      - Added some checks in Makefile to make sure people are using
      the custom OCaml (with all the extra files) and correct CAMLLIB CAMLP4LIB
      settings (Jason, you'll need to port this to omake!)
      
      - The check for ocamlopt will only be done when running "make opt" (or similar).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-18 22:33:57 -0700 (Fri, 18 Apr 2003)
Revision: 4458
Log message:

      More work on installation instructions.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-18 22:35:25 -0700 (Fri, 18 Apr 2003)
Revision: 4459
Log message:

      Later versions of make are OK too.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-18 22:37:16 -0700 (Fri, 18 Apr 2003)
Revision: 4460
Log message:

      "MetaPRL still has some nasty bugs" -> "MetaPRL could still have some nasty bugs"
      (I am hoping the most obvious ones were fixed by now).
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-04-19 02:52:01 -0700 (Sat, 19 Apr 2003)
Revision: 4461
Log message:

      got rid of all math_ terms defined for group theory in itt_comment.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-19 11:54:40 -0700 (Sat, 19 Apr 2003)
Revision: 4462
Log message:

      - Implemented resource annotations on rewrites (including conditional rewrites).
      - Implemented reduce resource annotations.
      - The annotations on ML rewrites are not supported (yet?), but at least they
      will now produce an error message, instead of being silently ignored.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-20 02:37:22 -0700 (Sun, 20 Apr 2003)
Revision: 4463
Log message:

      Replaced reduce resource "let" improvements with annotations, where
      possible.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-21 05:47:59 -0700 (Mon, 21 Apr 2003)
Revision: 4464
Log message:

      - If member_of{'a;'T} is declared, then "a in T" will be parsed as
      member_of{a;T} and will only fall back to equal{T;a;a} otherwise.
      
      - Bumped the rev nuumber for the CS101 version.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-04-21 14:57:41 -0700 (Mon, 21 Apr 2003)
Revision: 4465
Log message:

      Add filter_prog.ml to match Aleksey's last change.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-21 18:47:46 -0700 (Mon, 21 Apr 2003)
Revision: 4466
Log message:

      - Adding the theory and the proofs done in class today
      - instead of ``try "member_of", fall back to "equal"'' for (x in T) parsing,
      use ``try "equal", fall back to "member"'' strategy
      - A different symbol for "times" prl mode display (huge cross, even bigger than "X").
      Still ugly, but at least it's less confusing.
      - Fixed the df for resources with no args (it used to print an extra space).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-21 19:20:56 -0700 (Mon, 21 Apr 2003)
Revision: 4467
Log message:

      Added the new "member" form, other updates.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-22 02:04:30 -0700 (Tue, 22 Apr 2003)
Revision: 4468
Log message:

      - Added a real summary item for "define" directives. Now they are no longer
      implemented as simply "declare" + "prim_rw" and even the refiner now knows
      they are "special" (and, for example, status_all would not include them
      in a list of primitive rules/rewrites).
      
      - Make sure filter/Makefile does not need ocamldep binary on "make depend"
      (which is what it should be for non-leaf directories).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-22 02:45:03 -0700 (Tue, 22 Apr 2003)
Revision: 4469
Log message:

      Missed one incomplete match warning in my previous commit.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-22 15:35:58 -0700 (Tue, 22 Apr 2003)
Revision: 4470
Log message:

      Support files that have an .ml, but no .mli
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-04-22 17:27:43 -0700 (Tue, 22 Apr 2003)
Revision: 4471
Log message:

      Typo fixes
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-04-23 00:14:55 -0700 (Wed, 23 Apr 2003)
Revision: 4472
Log message:

      Typo fix.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-23 01:35:37 -0700 (Wed, 23 Apr 2003)
Revision: 4473
Log message:

      Simplified the term representation of the prec_rel summary item
      and made sure the display form actually corresponds to the representation used.
      

Changes by: ( at unknown.email)
Date: 2003-04-23 01:35:37 -0700 (Wed, 23 Apr 2003)
Revision: 4474
Log message:

      This commit was manufactured by cvs2svn to create tag 'CS101'.

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-23 01:55:28 -0700 (Wed, 23 Apr 2003)
Revision: 4475
Log message:

      Added basic documentation to the class lambda calc. theory.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-04-23 11:15:33 -0700 (Wed, 23 Apr 2003)
Revision: 4476
Log message:

      LN is now defined as "ln -s" so the "-f" flag is added manually.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-23 16:44:23 -0700 (Wed, 23 Apr 2003)
Revision: 4477
Log message:

      Stuff done in today's lecture.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-23 17:27:56 -0700 (Wed, 23 Apr 2003)
Revision: 4478
Log message:

      - Changed the diplsy form for "declare" to be nicer and to include both
      the raw and the dis[played version of the term.
      - Commented out the lucida fonts in the standard tex header in the tex
      printing functionality.
      - Added a script to print out all the CS101 theories into a .dvi
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-23 17:33:06 -0700 (Wed, 23 Apr 2003)
Revision: 4479
Log message:

      Printing script.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-04-23 18:03:52 -0700 (Wed, 23 Apr 2003)
Revision: 4480
Log message:

      Updated configuration as sub-project of mcc.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-23 23:27:07 -0700 (Wed, 23 Apr 2003)
Revision: 4481
Log message:

      Exporting declares to the interface, bumping the rev number.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-24 00:29:40 -0700 (Thu, 24 Apr 2003)
Revision: 4482
Log message:

      Yet another unicode symbol for "prod" (the one I chose before exists in RH9
      fonts, but not in RH7.3 ones)...
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-24 15:37:47 -0700 (Thu, 24 Apr 2003)
Revision: 4483
Log message:

      The MC theory is dead.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-24 17:29:42 -0700 (Thu, 24 Apr 2003)
Revision: 4485
Log message:

      Got rid of the HTML "tagges zone" code (which was used anyway).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-24 20:50:56 -0700 (Thu, 24 Apr 2003)
Revision: 4486
Log message:

      - Cleaned up a few display forms in IR
      - Started cleaning up the documentation in CPS
      - made cps resource improvement work through annotations.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2003-04-24 20:57:30 -0700 (Thu, 24 Apr 2003)
Revision: 4487
Log message:

      A few typo fixes and some work on the documentation for spill
      code.  I still need to clean up a few display forms and text.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-24 21:06:04 -0700 (Thu, 24 Apr 2003)
Revision: 4488
Log message:

      Minor updates (that provide a good demanstration of some bugs in MetaPRL
      text output mechanisms).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-24 21:28:18 -0700 (Thu, 24 Apr 2003)
Revision: 4489
Log message:

      - In lzone, do not stop printing once past the margin, let it wrap around,
      if necessary.
      - When displaing comments, display the normal math $...$ in lzone mode (e.g.
      let TeX do the line breaking).
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2003-04-24 22:00:12 -0700 (Thu, 24 Apr 2003)
Revision: 4490
Log message:

      The documentation for spill code looks a bit more reasonable.
      Up to silly typos that I have not caught, I think I am done with
      this bit of documentation.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-24 22:20:25 -0700 (Thu, 24 Apr 2003)
Revision: 4491
Log message:

      - Rformat: Added a notion of "tagged" boxes that need to be closed and re-opened
      on line break. The ensuremath macro is now implemented as a tagged box
      - Updated display forms so that the new dform for "declare" does not create
      problems of helper terms (such as those in the Comment theory).
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-04-25 03:22:09 -0700 (Fri, 25 Apr 2003)
Revision: 4492
Log message:

      minor.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-04-25 10:52:45 -0700 (Fri, 25 Apr 2003)
Revision: 4494
Log message:

      Some minor changes to the paper.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-04-25 15:34:01 -0700 (Fri, 25 Apr 2003)
Revision: 4498
Log message:

      Changed a rule about "onto homomorphism" to use "epimorphism".
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-04-25 15:50:19 -0700 (Fri, 25 Apr 2003)
Revision: 4499
Log message:

      Comitting small change.