Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-09-01 03:29:15 -0700 (Mon, 01 Sep 2003)
Revision: 4905
Log message:

      Fixed some typos in the documention.
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-09-01 08:00:09 -0700 (Mon, 01 Sep 2003)
Revision: 4906
Log message:

      Added magic/version to .cph file header.
      Now, before we do anything with .cph files, we check
      1. the magic number. If incorrect, we raise Bad_magic
      2. the version number. If incorrect, we use .pho file
      3. if header checks out, we use .cph file (of course, we check
      whether the .pho file is newer or not)
      
      Also, got rid of precedence warnings. This was a check to ensure that
      all prec directives list terminal symbols. This is too conservative,
      so I removed it entirely. I will modify this in my next commit to
      check whether all rules with %prec name valid precedence symbols,
      e.g. either existing terminal symbols or those listed in the precedence
      section.
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-09-01 08:37:18 -0700 (Mon, 01 Sep 2003)
Revision: 4907
Log message:

      Check whether we specify valid symbols in %prec of a rule.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-09-01 16:46:00 -0700 (Mon, 01 Sep 2003)
Revision: 4908
Log message:

      Document all magic numbers in a single location.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-09-01 16:59:50 -0700 (Mon, 01 Sep 2003)
Revision: 4909
Log message:

      Typo fixes in the documentation.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-09-01 20:28:23 -0700 (Mon, 01 Sep 2003)
Revision: 4910
Log message:

      Cleaning up and refactoring the refiner implementation.
      
      Now refiner should keep enough information around to be able
      to figure out which axioms a proof is dependent on.
      
      Still to do: need to be able to actually extract out the dependency
      information and a UI to print it (including UI for checking whether
      teh rule is fully grounded or not).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-09-02 19:57:45 -0700 (Tue, 02 Sep 2003)
Revision: 4911
Log message:

      Xin & Aleksey:
      - Fixed and improved a number of display forms.
      - Made a number of improvements to the documentation text.
      - Fixed the recent breakage in Itt_rfun (removed the ``experimental'' rule
      that Xin have added and removed the unneeded assumption from the original rule).
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2003-09-02 20:39:39 -0700 (Tue, 02 Sep 2003)
Revision: 4912
Log message:

      Build-system changes for PREBUILT_CLIBS option.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2003-09-02 20:40:17 -0700 (Tue, 02 Sep 2003)
Revision: 4913
Log message:

      Build system changes for PREBUILT_CLIBS option.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-09-03 00:54:38 -0700 (Wed, 03 Sep 2003)
Revision: 4914
Log message:

      Working on the MetaPRL publications page.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-09-03 14:34:13 -0700 (Wed, 03 Sep 2003)
Revision: 4915
Log message:

      Copy files from the $(PREBUILT_CLIBS) directory.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-09-03 15:47:35 -0700 (Wed, 03 Sep 2003)
Revision: 4916
Log message:

      Disable the display of cache status for now.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-09-03 17:24:37 -0700 (Wed, 03 Sep 2003)
Revision: 4917
Log message:

      A newer config.win32
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-09-03 17:26:43 -0700 (Wed, 03 Sep 2003)
Revision: 4918
Log message:

      Updated the .INCLUDE lines.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-09-03 18:09:20 -0700 (Wed, 03 Sep 2003)
Revision: 4919
Log message:

      - Adding TPHOLs cat B papers.
      - Adding PDF and PS for the TPHOLs cat A system description.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-09-03 18:47:39 -0700 (Wed, 03 Sep 2003)
Revision: 4920
Log message:

      I think I solved the problem with regenerating mk/config!
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-09-03 18:54:14 -0700 (Wed, 03 Sep 2003)
Revision: 4921
Log message:

      Better comments.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-09-03 19:46:38 -0700 (Wed, 03 Sep 2003)
Revision: 4922
Log message:

      Added Alexei's dependent intersection paper.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-09-03 19:54:03 -0700 (Wed, 03 Sep 2003)
Revision: 4923
Log message:

      Adding ISSRE paper (without any abstract or electronic version for now).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-09-03 20:18:06 -0700 (Wed, 03 Sep 2003)
Revision: 4924
Log message:

      Added Jason's CADE system discription. I've added a link to the Springer's site
      (with the PDF of Jason's paper), but no local electronic copies. Jason, do
      you have any electronic copies we can put on files.metaprl.org?
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-09-03 20:38:41 -0700 (Wed, 03 Sep 2003)
Revision: 4925
Log message:

      Added the original Nuprl-Light paper.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-09-03 20:58:25 -0700 (Wed, 03 Sep 2003)
Revision: 4926
Log message:

      Adding the paper on FOrmal Design Environment
      Adding the papers page to the MetaPRL navigation.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-09-03 21:07:56 -0700 (Wed, 03 Sep 2003)
Revision: 4927
Log message:

      Adding the MERLIN paper.
      
      Jason, do you have any bibliographical information for this one? Thanks!
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-09-03 21:11:28 -0700 (Wed, 03 Sep 2003)
Revision: 4928
Log message:

      Implemented versioning, check_config, etc.
      
      CAUTION: you will need the latest version of omake to do this, since
      it defines new functions needed during versioning.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-09-04 03:05:41 -0700 (Thu, 04 Sep 2003)
Revision: 4929
Log message:

      Changed the Refine.extract to contain a pointer to the sentinel used to
      create the extract, which in turn contains a pointer to the refiner.
      Using these pointer, we garantee that in any extract all parts were
      created using the same sentinel and that a derived rule can only be justified
      by an extract that was created using the appropriate refiner.
      
      Note - this may cause problems when construction extract from a distributed proof,
      as Refine module now expects things to be pointer-equal...
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-09-04 04:23:25 -0700 (Thu, 04 Sep 2003)
Revision: 4930
Log message:

      I have implemented parsing of the proofs and extraction of the information
      on which axioms a certain proof depends (producing an error message if
      a proof uses - directly or indirectly - a derived item that was not fully
      proven). Note that the scanning is done xon the lowest possible level (Refine
      module), so the results are high-confidence.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-09-04 14:32:58 -0700 (Thu, 04 Sep 2003)
Revision: 4931
Log message:

      Added an alias for "it" - "trivial".
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-09-04 16:00:38 -0700 (Thu, 04 Sep 2003)
Revision: 4932
Log message:

      Killing the PREBUILT_CLIBS flag.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-09-04 17:14:55 -0700 (Thu, 04 Sep 2003)
Revision: 4933
Log message:

      This fixed bug 32 - "omake clean" now really cleans everything in needs to clean
      and "omake realclean" now only prompts about .omakedb, and mk/config* files.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-09-05 00:10:12 -0700 (Fri, 05 Sep 2003)
Revision: 4935
Log message:

      - Changed the way mp_version.ml is hapdled to be a -pp hack on a static .ml file.
      This will likely break Win32 build! :-(
      
      - Added checks that make sure that the extract passed into Refiner really proves
      what it was supposed to prove. This requires moving a HACK that creates sequent
      representation of rewrites into the Refine module :-(
      

Changes by: ( at unknown.email)
Date: 2003-09-05 00:10:12 -0700 (Fri, 05 Sep 2003)
Revision: 4936
Log message:

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

Changes by: ( at unknown.email)
Date: 2003-09-05 00:10:12 -0700 (Fri, 05 Sep 2003)
Revision: 4937
Log message:

      This commit was manufactured by cvs2svn to create branch
      'new-then_Lab_T-implementation'.

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-09-05 07:43:00 -0700 (Fri, 05 Sep 2003)
Revision: 4938
Log message:

      Turn off threads.  We need them only for the threaded refiner and the
      http server.  Sometime, we should figure out how to get the build
      system to enable/disable threads.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-09-05 08:30:16 -0700 (Fri, 05 Sep 2003)
Revision: 4939
Log message:

      MetaPRL compiles and runs on Cygwin.
      Now, I need to figure out the font situation.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-09-05 10:37:53 -0700 (Fri, 05 Sep 2003)
Revision: 4940
Log message:

      Extraction finally works!!!!!!!!!!
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-09-05 15:25:56 -0700 (Fri, 05 Sep 2003)
Revision: 4941
Log message:

      Start with empty MPFILES.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-09-05 17:47:10 -0700 (Fri, 05 Sep 2003)
Revision: 4942
Log message:

      For tutorial, refreshing most .prla files in base and itt.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-09-05 17:53:19 -0700 (Fri, 05 Sep 2003)
Revision: 4943
Log message:

      Killing the old tutorial, replacing all links to it with links to
      http://files.metaprl.org/papers/tutorial1.pdf
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-09-05 17:54:11 -0700 (Fri, 05 Sep 2003)
Revision: 4944
Log message:

      No tutorial anymore.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-09-05 18:06:59 -0700 (Fri, 05 Sep 2003)
Revision: 4945
Log message:

      Version 0.9.5!!!
      

Changes by: ( at unknown.email)
Date: 2003-09-05 18:06:59 -0700 (Fri, 05 Sep 2003)
Revision: 4946
Log message:

      This commit was manufactured by cvs2svn to create tag
      'metaprl-0_9_5'.

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-09-05 18:15:18 -0700 (Fri, 05 Sep 2003)
Revision: 4947
Log message:

      The version 0.9.5 is now tagged with CVS tag "metaprl_0_9_5" and I am
      changing the version string to 0.9.5+ to make sure that only this exact
      version of MetaPRL calls itself 0.9.5.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-09-09 03:28:06 -0700 (Tue, 09 Sep 2003)
Revision: 4948
Log message:

      - NCURSES should be on by default
      - Add a comment to mk/config to let people know that NCURSES should
      be enabled in order for READLINE to work