Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-01 17:14:04 -0800 (Wed, 01 Dec 2004)
Revision: 6297
Log message:

      The magic number needed to be updated.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-01 18:12:20 -0800 (Wed, 01 Dec 2004)
Revision: 6298
Log message:

      Omake will now monitor some of the files and warn if filter/base/filter_magic.ml
      may need to be updated.
      
      This is loosely based on the new_parser2 branch.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-01 18:26:16 -0800 (Wed, 01 Dec 2004)
Revision: 6299
Log message:

      filter/base/filter_type.mlz should be included in the magic number computation.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-01 18:41:11 -0800 (Wed, 01 Dec 2004)
Revision: 6300
Log message:

      A bunch of minor fixes in comments, formatting, etc.
      (Merging some of the cosmetical changes made by Jason in the new_parser branch).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-01 18:48:14 -0800 (Wed, 01 Dec 2004)
Revision: 6301
Log message:

      Use Digest.to_hex instead of a custom conversion to an int (which produced
      different results on 32-bit and 64-bit platforms).
      

Changes by: ( at unknown.email)
Date: 2004-12-01 18:48:14 -0800 (Wed, 01 Dec 2004)
Revision: 6302
Log message:

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

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-01 19:20:34 -0800 (Wed, 01 Dec 2004)
Revision: 6303
Log message:

      A new incarnation of the new_parser branch (off of the current trunk).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-01 19:43:07 -0800 (Wed, 01 Dec 2004)
Revision: 6304
Log message:

      (new_parser merge) comment/formatting change.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-12-01 21:31:24 -0800 (Wed, 01 Dec 2004)
Revision: 6305
Log message:

      GENMAGIC = $(BIN)/genmagic$(EXE)
      was missing $(EXE)  suffix
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-12-02 00:22:28 -0800 (Thu, 02 Dec 2004)
Revision: 6306
Log message:

      fixed
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-02 12:14:29 -0800 (Thu, 02 Dec 2004)
Revision: 6307
Log message:

      Use NF instaed of just 4.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-02 16:02:19 -0800 (Thu, 02 Dec 2004)
Revision: 6313
Log message:

      Renamed GramUpd -> MLGramUpd, Grammar -> PRLGrammar
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-02 16:55:41 -0800 (Thu, 02 Dec 2004)
Revision: 6314
Log message:

      Pretty-print Lm_parser.ParseError
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-02 17:11:41 -0800 (Thu, 02 Dec 2004)
Revision: 6315
Log message:

      Changed the action id to be gensym-based instead of location-based
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-02 17:38:16 -0800 (Thu, 02 Dec 2004)
Revision: 6316
Log message:

      Merging Jason's mmc_parser branch.
      
      This adds a new Libmojave/rewriter-based parser similar to Phobos.
      The advantage of this new parser (compared to Phobos) is that it is
      much better integrated to the rest of the filter. In particular:
       - New-style grammar specifications reside in .mli and .ml, and not
         in a separate .pho file (note - .mli grammars are inherited; .ml ones
         are local)
       - The opname management is reused (no need to re-declare opnames in the
         grammar specifications).
       - Grammars are saved in the .cmoz/.cmiz instead of a separate file.
       - Grammars are properly scoped (and toploop knows about it).
       - Grammars are inherited along the module inheritance hierarchy
         and can be extended by the children.
       - Instead of a single "<:ext<" grammar, arbitrarily-named grammars may be
         defined.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-02 18:26:23 -0800 (Thu, 02 Dec 2004)
Revision: 6317
Log message:

      The new parser branch have added a "token" keyword which clashed with a number
      of places using the "token" for other things (opname, type, etc). I've renamed
      the "token" keyword into "lex_token".
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-03 12:57:11 -0800 (Fri, 03 Dec 2004)
Revision: 6319
Log message:

      Unused variable.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-12-03 20:53:07 -0800 (Fri, 03 Dec 2004)
Revision: 6320
Log message:

      Now SupInf handles trivially contradictory inequalities correctly (like 0>5)
      and quickly, before it was completely missing them because of the design.
      In particular, it now proofs inttestn/1.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-03 21:14:31 -0800 (Fri, 03 Dec 2004)
Revision: 6321
Log message:

      Removed a bit of temporary code from the ascii_io module.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-12-03 22:01:44 -0800 (Fri, 03 Dec 2004)
Revision: 6322
Log message:

      Proved all testcases
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-03 22:04:09 -0800 (Fri, 03 Dec 2004)
Revision: 6323
Log message:

      - mllib/OMakefile and mllib/Files both had (different) lists of .mlz
      files, inlining Files for simplicity and consistency (now that we no
      longer use make, we should be getting rid of the "Files" files).
      
      - filter_type had "MAGICBEGIN" marker a bit too early (no need to MD5
      the expections).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-03 22:24:41 -0800 (Fri, 03 Dec 2004)
Revision: 6324
Log message:

      Fixed some issues in the ocaml <-> term conversion.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-03 22:47:42 -0800 (Fri, 03 Dec 2004)
Revision: 6325
Log message:

      Fixing a bug in fv computation (we've hever hit it, but it's potentially nasty).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-03 23:48:48 -0800 (Fri, 03 Dec 2004)
Revision: 6326
Log message:

      There is no need to name individual punctuation symbols in the term grammar.
      
      Note that this no-op commit dramatically reduces the compile time for this
      file. On Mojave clients, compiling just this one file use to take about a
      minute and now it is down to less than 20 seconds!
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-03 23:54:21 -0800 (Fri, 03 Dec 2004)
Revision: 6327
Log message:

      Minor fixes in dest_context/mk_context functions.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-04 00:27:38 -0800 (Sat, 04 Dec 2004)
Revision: 6328
Log message:

      Fixing an error message
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-04 00:36:58 -0800 (Sat, 04 Dec 2004)
Revision: 6329
Log message:

      Fixed the "let v = t1 in t2" syntax.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-04 01:12:47 -0800 (Sat, 04 Dec 2004)
Revision: 6330
Log message:

      - Fixed a few minor bugs in handling of non-sequent contexts.
      
      - Added an input syntax for non-sequent context terms
        ( 'V<|C;...;C|>[[t]][t;...;t], where "<|...|>" and "[...]" are optional)
      
      Note that this is only a small part of what will be needed to fully support
      non-sequent contexts. The rewriter and filter code for non-sequent contexts is
      still incomplete (the biggest problem is that we currently only allow term and
      int paramaters in primitive rules, while non-sequent contexts require address
      parameters) and would not work.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-12-04 13:16:54 -0800 (Sat, 04 Dec 2004)
Revision: 6331
Log message:

      Forgot to skip trivial inequalities like 5>0 (since I detect things like 0>5,
      it's logical to skip 5>0-likes)
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-12-04 14:02:32 -0800 (Sat, 04 Dec 2004)
Revision: 6332
Log message:

      This commit (w->wb) fixes a problem caused by
      http://cvs.cs.cornell.edu:12000/commitlogs/metaprl/2004-12.html#04/12/01.21:48:14
      under win32.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-06 17:10:10 -0800 (Mon, 06 Dec 2004)
Revision: 6333
Log message:

      Removed reduce_fix and reduce_ycomb from the reduce resource (to avoid
      infinite loops in reduceC, reduceT, byDefT, etc).
      
      Alexei: this broke /itt_record0/recordTIntro1, please take a look.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-06 17:14:08 -0800 (Mon, 06 Dec 2004)
Revision: 6334
Log message:

      Proved are_compatible_shapes_aux_wf
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2004-12-06 17:43:13 -0800 (Mon, 06 Dec 2004)
Revision: 6335
Log message:

      Fixed /itt_record0/recordTIntro1
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-06 18:09:15 -0800 (Mon, 06 Dec 2004)
Revision: 6336
Log message:

      (bug 181) Auto-generate the list of the include directories.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-06 20:35:31 -0800 (Mon, 06 Dec 2004)
Revision: 6337
Log message:

      Rewrote the proof squashing code. Hopefully this will fix bug 160 and other
      relatex issues.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-06 21:48:40 -0800 (Mon, 06 Dec 2004)
Revision: 6338
Log message:

      Made the "toggle" button really toggle. When the "Long" button is clicked
      on, its text now changes to "Short" and clicking on "Short" restores the
      commandline input field and the "Long" label.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-07 19:41:40 -0800 (Tue, 07 Dec 2004)
Revision: 6340
Log message:

      Fixed a few quoting issues with JS menus (including the ' symbol in command
      line history).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-07 23:30:09 -0800 (Tue, 07 Dec 2004)
Revision: 6341
Log message:

      Unset debug_rewrite while inside the print_term.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-07 23:49:05 -0800 (Tue, 07 Dec 2004)
Revision: 6342
Log message:

      Rearranged and cleaned up the code a bit.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-12-08 12:15:25 -0800 (Wed, 08 Dec 2004)
Revision: 6343
Log message:

      Parsing documentation.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-08 19:45:46 -0800 (Wed, 08 Dec 2004)
Revision: 6344
Log message:

      Fixing some of the HTML syntax violations.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-08 20:12:53 -0800 (Wed, 08 Dec 2004)
Revision: 6345
Log message:

      Turns out that for some reason Firefox has problem with JS making the
      iframe size _bigger_ than the css value, but has no poblem making it
      _smaller_. So a workaround for some of the weird Firefox issues is to
      start with very large initial CSS values of "height" (since they get
      overriden by JS anyway it should not matter on other browsers).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-08 21:23:30 -0800 (Wed, 08 Dec 2004)
Revision: 6346
Log message:

      Allow nth_hyp annotation on H >- t1 --> H >- t2 rules.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-08 23:24:13 -0800 (Wed, 08 Dec 2004)
Revision: 6347
Log message:

      Browser interface fixes:
      - Menu labels need to be HTML escaped.
      - "slot" mechanism should use the "src" display forms form the local theory,
        not for the "top" bookmark.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-08 23:41:52 -0800 (Wed, 08 Dec 2004)
Revision: 6348
Log message:

      Removed the wf hypothesis from the bterm_elim2 rule. Xin, I am leaving the
      bterm_elim2 and bterm_elim3 to you.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-12-09 22:45:54 -0800 (Thu, 09 Dec 2004)
Revision: 6349
Log message:

      with this commit [try]onAll[M][Cumulative]HypsT, onSomeHypT and
      onAllMClausesOfAssumT skip contexts automatically.
      As far as I understand this commit didn't affect any proofs.
      It's possible that now some occurences of tryOnAll... can be replaced with
      onAll...
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-12-09 22:59:54 -0800 (Thu, 09 Dec 2004)
Revision: 6350
Log message:

      1. I believed that with this commit and bug 361 fixed
      mldebug.dir and theories.dir will be generated correctly for win32.
      bat-files have new set-commands, they just have to be uncommented
      (and old one removed)
      2. I also replaced (again) hard-coded paths to SSL library under win32
      with variables that can be set in mk/config.local
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-09 23:27:21 -0800 (Thu, 09 Dec 2004)
Revision: 6351
Log message:

      Simplified some of the .dir creation code a bit
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-10 01:45:32 -0800 (Fri, 10 Dec 2004)
Revision: 6352
Log message:

      (Bug 363) Typing would now bring focus to the command line input form. As
      usual with JS, part of this is an ugly hack - finding out what character was
      typed (in order to append it to the command line) is not easy and involves
      things like manually testing the state of the Shift key :-(
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-12-10 11:23:54 -0800 (Fri, 10 Dec 2004)
Revision: 6353
Log message:

      Forgot to remove old versions of supporting code for onAllHyps-tacticals
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-12-10 12:50:28 -0800 (Fri, 10 Dec 2004)
Revision: 6354
Log message:

      Backport to Win2000.  The .dir stuff still doesn't work, and this
      includes a hack to get around Yegor's changes to SSL config.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-10 12:58:52 -0800 (Fri, 10 Dec 2004)
Revision: 6355
Log message:

      Moved the SSL_WIN32 stuff to mk/defaults so that it can still be overridden
      in mk/config.local
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-12-12 02:33:42 -0800 (Sun, 12 Dec 2004)
Revision: 6356
Log message:

       - Added the var_bterm case support for make_bterm in base_reflection.
       - Fixed some bugs in itt_reflection; Added some primitive rules.
      
      The four lemmas for "subst_make_bterm" haven't been proved yet.
      
      Just want to do the commit before fixing this bug:
      ---------
        Do we consider these two bterms are the same?
           1. 'b1 = bterm{| x: term >- it[@] |}
           2. 'b2 = bterm{| >- it[@] |}
      
        If yes, then we should modify the definition of if_simple_bterm.
      
        If no, then "makebterm_same_op" is not valid, since
           make_bterm { 'b1; [] } <-->
           make_bterm{ 'b1; subterms{'b1} } <-->
           'b1
        and
           make_bterm{ 'b1; [] } <-->
           make_bterm{ 'b1; subterms{'b2} } <-->
           'b2
        which gives
           'b1 <--> 'b2
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-12-13 15:42:09 -0800 (Mon, 13 Dec 2004)
Revision: 6357
Log message:

      consSquiddleEq shouldn't be primitive.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-15 16:30:05 -0800 (Wed, 15 Dec 2004)
Revision: 6358
Log message:

      Escape spaces in file/directory names.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-17 00:50:01 -0800 (Fri, 17 Dec 2004)
Revision: 6359
Log message:

      (Bug 200 follow-up) fixed a few places where html display forms caused
      invalid HTML to be generated on MetaPRL pages.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-12-17 13:23:37 -0800 (Fri, 17 Dec 2004)
Revision: 6360
Log message:

      Minor fixes.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-12-28 11:22:55 -0800 (Tue, 28 Dec 2004)
Revision: 6361
Log message:

      1. Omega Test added. It's not a complete implementation of the original Omega
      Test (splinters are not implemented hence it's not a complete procedure).
      In the current state it seems to be a little weaker than SupInf.
      Implementation is very straightforward, many optimizations from Pugh's paper
      are not implemented.
      
      2. All tests from itt_int_arith and itt_supinf are moved to itt_int_test
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-12-28 11:55:53 -0800 (Tue, 28 Dec 2004)
Revision: 6362
Log message:

      gen_int_bench generates two benchmarks itt_int_bench and itt_int_bench2
      for arithmetical tactics.
      On those tests SupInf consumes more than 400Mb and I have to terminate it
      (I will investigate if memory consumption can be optimized)
      Omega Test proves about 50% of tests (5 out of 10, they are not guaranteed to be provable)
      in 50 and 40 seconds respectfully consuming about 100Mb.
      Unfortunately on the other 50% of tests Omega crashes MetaPRL (under Cygwin) -
      will investigate.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-12-28 12:05:53 -0800 (Tue, 28 Dec 2004)
Revision: 6363
Log message:

      *.lnk should be ignored (used under Cygwin)
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-12-28 12:07:16 -0800 (Tue, 28 Dec 2004)
Revision: 6364
Log message:

      *.stackdump and *.o have to be ignored
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-12-28 14:31:51 -0800 (Tue, 28 Dec 2004)
Revision: 6365
Log message:

      Hopyfully this will fix the problem introduced by my previous commit
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-28 17:09:45 -0800 (Tue, 28 Dec 2004)
Revision: 6366
Log message:

      Another update of the OMakefile.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-28 21:58:46 -0800 (Tue, 28 Dec 2004)
Revision: 6367
Log message:

      Fixed some of the issues with duplicated and/or absolute paths in
      OCAMLINCLUDES. Should fix (or rather work around) bug 372, could also fix bug
      373.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-12-29 14:04:01 -0800 (Wed, 29 Dec 2004)
Revision: 6368
Log message:

      It is unsafe to use $(ROOT) because when metaprl is in the root directory
      $(ROOT)/XXX is //XXX and cause problems (with GCC)
      
      May be $(dir /) should evaluate to empty string (or may be to "/.") rather than to "/" ?
      

Changes by: Nataly Novak (nnovak at gc.cuny.edu)
Date: 2004-12-30 10:47:38 -0800 (Thu, 30 Dec 2004)
Revision: 6369
Log message:

      We are exploring another approach - instead of giving universal rules for cases
      analysis and fixpoint we want to generate specific instances of these rules for
      individual inductive types automatically.
      

Changes by: Nataly Novak (nnovak at gc.cuny.edu)
Date: 2004-12-30 12:51:22 -0800 (Thu, 30 Dec 2004)
Revision: 6370
Log message:

      minor bug is fixed
      

Changes by: Nataly Novak (nnovak at gc.cuny.edu)
Date: 2004-12-30 12:54:11 -0800 (Thu, 30 Dec 2004)
Revision: 6371
Log message:

      Working on automatic generation of case-analysis rules
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-12-30 13:12:04 -0800 (Thu, 30 Dec 2004)
Revision: 6372
Log message:

      According to Aleksey, $(LIB) should be avoided
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-30 21:17:20 -0800 (Thu, 30 Dec 2004)
Revision: 6373
Log message:

      Avoid having to symlink/copy libs into the lib directory just to compile
      MetaPRL.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-31 14:41:33 -0800 (Fri, 31 Dec 2004)
Revision: 6374
Log message:

      Reverting an accidental commut.