Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-01 08:43:39 -0700 (Tue, 01 Jun 2004)
Revision: 5842
Log message:

      Added lm_uname, a hook to the uname syscall.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-01 13:11:56 -0700 (Tue, 01 Jun 2004)
Revision: 5843
Log message:

      Updated the OMakefiles to see if we can get threads working again.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-01 19:34:11 -0700 (Tue, 01 Jun 2004)
Revision: 5844
Log message:

      Updating the make build system to support THREADS_ENABLED.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-01 19:46:55 -0700 (Tue, 01 Jun 2004)
Revision: 5845
Log message:

      - added a generated file to "make clean"
      - use "rm; ar cq" (same as omake) instead of "ar r" (which prints annoying messages).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-01 20:39:05 -0700 (Tue, 01 Jun 2004)
Revision: 5846
Log message:

      Fixing bug 221 - made the Phobos pp functionality more consistent.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-01 22:19:28 -0700 (Tue, 01 Jun 2004)
Revision: 5847
Log message:

      More profiling support.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-01 22:32:50 -0700 (Tue, 01 Jun 2004)
Revision: 5848
Log message:

      "omake clean" should be a bit more clean.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-06-02 00:21:15 -0700 (Wed, 02 Jun 2004)
Revision: 5849
Log message:

      Other places requiring quote-parameter update.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-06-02 00:36:03 -0700 (Wed, 02 Jun 2004)
Revision: 5850
Log message:

      Removed unnecessary changes in 1.31.2.2
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-04 12:23:54 -0700 (Fri, 04 Jun 2004)
Revision: 5851
Log message:

      This update is just a rearrangement of the code to make it a bit more manageable:
      - Moved a number of common types from Proof_edit to Shell_sig (the types are
        all related and it is nice to have them in the same place).
      - Inlined package_sig.mlz into package_info.mli (since we had a signature that
      was only referred to once).
      - Inlined Package_info.Package into Package_info (no need to have extra
      indirection).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-04 14:26:57 -0700 (Fri, 04 Jun 2004)
Revision: 5852
Log message:

      Removing some unused code (because it is using some APIs that I want
      to make private).
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-06-04 14:50:05 -0700 (Fri, 04 Jun 2004)
Revision: 5853
Log message:

      Alexei&Xin:
      Added "@" for quote parameter.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-04 15:43:14 -0700 (Fri, 04 Jun 2004)
Revision: 5854
Log message:

      Cert generation prints a lot of junk; redirecting it to /dev/null.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-04 16:12:47 -0700 (Fri, 04 Jun 2004)
Revision: 5855
Log message:

      (Merging the quote_param branch)
      This commit is a first step towards adding reflective reasoning capabilities
      to MetaPRL. This adds:
      - a "Quote" parameter (represented as "@" on I/O)
      - support for basic quoting/unquoting (no variable or sequent support yet) to
        the term modules.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-04 16:54:27 -0700 (Fri, 04 Jun 2004)
Revision: 5856
Log message:

      Removing some unused code that attempted to duplicate functionality already
      existing elsewhere.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-06-05 18:26:21 -0700 (Sat, 05 Jun 2004)
Revision: 5857
Log message:

      reduce_add_monom is more strict now (does not rely on implicit assumptions)
      all rewrites added to .mli for profiling
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-06-05 22:04:10 -0700 (Sat, 05 Jun 2004)
Revision: 5858
Log message:

      minor changes
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-06-06 09:08:04 -0700 (Sun, 06 Jun 2004)
Revision: 5859
Log message:

      Added a slight improvement.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-06-06 20:48:24 -0700 (Sun, 06 Jun 2004)
Revision: 5860
Log message:

      more optimization (treatment of wf-subgoals is optimal now,
      itt_mpoly2_bench is 5 times slower than itt_int_arith)
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-06-08 20:17:17 -0700 (Tue, 08 Jun 2004)
Revision: 5861
Log message:

      Fixing some proofs that were borken long ago - when I forked evaluation to
      a separate (from reduceC) resource.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-06-08 20:45:26 -0700 (Tue, 08 Jun 2004)
Revision: 5862
Log message:

      *.o added
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-06-08 20:49:14 -0700 (Tue, 08 Jun 2004)
Revision: 5863
Log message:

      Added one more version with no intermediate conversions
      (from reflected terms to polynomials) at all but efficency is exactly same as
      in itt_mpoly2(_bench). Will look for possible optimizations.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-08 23:25:24 -0700 (Tue, 08 Jun 2004)
Revision: 5864
Log message:

      Some code cleanup.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-09 00:01:59 -0700 (Wed, 09 Jun 2004)
Revision: 5865
Log message:

      Correctly normalize the proof node when taking a node count (the code that was
      supposed to do it used to be incomplete).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-09 00:51:43 -0700 (Wed, 09 Jun 2004)
Revision: 5866
Log message:

      Proved pairFormation from pairEquality.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-09 01:55:08 -0700 (Wed, 09 Jun 2004)
Revision: 5867
Log message:

      The Itt_dprod.productSubtype rule was invalid! I've added the missing wf
      assumption and turned the rule from an invalid prim to a proven
      interactive one.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-09 10:53:06 -0700 (Wed, 09 Jun 2004)
Revision: 5868
Log message:

      Minor code clean-up.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-09 11:38:02 -0700 (Wed, 09 Jun 2004)
Revision: 5869
Log message:

      This modifies the infrastructure for threads.  Here is the model:
      
          1. Each thread has a current state, and each state has a set
             of global variables.
      
          2. State variables must be locked before being used.
      
          3. State variables come in two types: shared and private.
             Each state has its own copy of the private variables.
      
      For example, each job in the shell has its own state, and its
      own copy of the Shell.info struct.  States are managed implicitly,
      so global variables look just like global variables.  Access is
      managed with the State.read/State.write routines.
      
      Here is an example of usage for a shared variable:
      
          let global_entry = State.shared_val "debug" (ref 0)
      
          let get () =
             State.read global_entry (fun x -> !x)
      
          let incr () =
             State.write global_entry (fun x -> x := !x + 1)
      
      For private variable, you have to supply a "fork" function that
      is used to copy the value.  Each thread/state will have its own copy
      of the variable.  The other functions remain the same.
      
          let global_entry = State.shared_val "debug" (ref 0) (fun x -> ref !x)
      
      All the State.* functions are wrappers that take a function argument.  The
      value is locked on entry into the function, and unlocked when the function exits.
      Exceptions are handled correctly.
      
      Don't use Mutex if you can help it!!!  The Mutex functions do not
      handle exceptions correctly.  Use the State module instead.
      
      NOTES:
      
         1. I removed the Java interface...  It was just getting to be too much
            of a hassle.  We can ressurect it if we ever want it again.
      
         2. This is just the infrastructure pass.  The global values used by the
            browser need to be updated to the new model.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-09 13:56:34 -0700 (Wed, 09 Jun 2004)
Revision: 5870
Log message:

      Updated the browser to the new state model.
      
      Note: we still get less parallelism than we would hope, because
      refinement shares the (unique) output channel.  This could be fixed
      by making stdout/stderr private variables.  Or we could just accept
      that output will be jumbled if multiple threads are running.
      
      I haven't actually enabled multiple threads yet in Http_simple.
      That's next.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-09 17:52:47 -0700 (Wed, 09 Jun 2004)
Revision: 5871
Log message:

      Added a "find_subgoal" tool for finding the primitive node that generated
      the given subgoal. This should be a great tactic debugging tool.
      
      Basically, when you at a node (whether a rule box, or an internal "address 0"
      one) on the form
      
         Goal Term
      
         BY ...
      
         1. Subgoal Term
         2. Subgoal Term
         ...
      
      then "find_subgoal 0" would take you to the node that generated the goal term
      (i.e. it would go up towards the root of the proof tree), the "find_subgoal 1"
      would take you to the node that _first_ generated the subgoal 1 term (if
      goal happens to be the same as subgoal 1, then it would still go up the tree;
      otherwise it would "zoom into" the current node).
      
      P.S. This code is not fully debugged, there still might be an "off by one" error
      somewhere.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-09 19:02:18 -0700 (Wed, 09 Jun 2004)
Revision: 5872
Log message:

      Simplified the code a bit (by moving the commands record hack into the
      Top submodule).
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-06-09 19:55:35 -0700 (Wed, 09 Jun 2004)
Revision: 5873
Log message:

      Interestingly that for this version lazy strategy (like in reduceC)
      is more efficient than more eager strategy used in itt_mpoly2.
      Now itt_mpoly3_bench/test* is 4 times slower than itt_int_arith/test*.
      Actually the most complicated "testn" only 2 times slower but simpler
      examples have obviously worse factor.
      
      I realized that we can't expect same performance from this approach
      as normalizeC has because normalizeC is combination of ml-code and
      rewrites but itt_mpoly* use only rewrites for normalization.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-10 09:55:11 -0700 (Thu, 10 Jun 2004)
Revision: 5874
Log message:

      Declare the loc version of the resource_def.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-10 13:45:08 -0700 (Thu, 10 Jun 2004)
Revision: 5875
Log message:

      This implements a version of SLOPPY_DEPENDENCIES.  Sloppy dependencies
      use a dummpy file .sloppy.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-10 14:53:34 -0700 (Thu, 10 Jun 2004)
Revision: 5876
Log message:

      Resolved the Not_found problem.  So hard to track down:(
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-10 15:06:02 -0700 (Thu, 10 Jun 2004)
Revision: 5877
Log message:

      Removing some slot terms.  Note that anything displayed in a slot
      is selectable from the browser.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-10 15:51:04 -0700 (Thu, 10 Jun 2004)
Revision: 5878
Log message:

      Updated a few display forms (including one for sequents and meta-sequents)
      to use slot{} in the right places.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-10 16:36:41 -0700 (Thu, 10 Jun 2004)
Revision: 5879
Log message:

      - Do not use slot{} in Perv!cons display form
      - Do not use slot{} in Comments display forms
      - Do use slot{} when displaying subterms of an SO var.
      
      Ths problem with slot in comments (especially with the slot{'cdr} in the
      Perv!cons display form) is that HTML has a limit on the level of nested tags -
      the tags can only be nested up to 100 deep. We were exceeding this limit on
      comments.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-10 17:01:13 -0700 (Thu, 10 Jun 2004)
Revision: 5880
Log message:

      View options should now be more sensible.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-10 22:26:34 -0700 (Thu, 10 Jun 2004)
Revision: 5881
Log message:

      Got rif of the unused "internal" flag for the display forms.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-11 03:23:07 -0700 (Fri, 11 Jun 2004)
Revision: 5882
Log message:

      Removed a huge number of repeatitions of
      try getenv "MPLIB" with ...
      Now the Env_arg module is the "authoritative" source for this.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-11 09:33:41 -0700 (Fri, 11 Jun 2004)
Revision: 5883
Log message:

      Synchronization fixes.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-11 11:05:55 -0700 (Fri, 11 Jun 2004)
Revision: 5884
Log message:

      Stype tweaks to get resizing to work better.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-11 13:09:32 -0700 (Fri, 11 Jun 2004)
Revision: 5885
Log message:

      Adding support for saving session state in files.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-11 18:23:11 -0700 (Fri, 11 Jun 2004)
Revision: 5886
Log message:

      Moved the initialization of common paths ($MPLIB, $MP_HOME, ~/.metaprl, etc)
      into the mllib/setup module.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-11 19:11:06 -0700 (Fri, 11 Jun 2004)
Revision: 5887
Log message:

      Made the Setup.lib and Setup.root computation delayed (to allow the setup
      module in proxyedit, and having it work without MPLIB defined).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-11 20:46:13 -0700 (Fri, 11 Jun 2004)
Revision: 5888
Log message:

      - (bug 154) Made the read_tokens function delayed - the token file will
      not be read until an FDL connection is actually opened.
      
      - The filter-processes MetaPRL files no longer depend on the phony
      $(MPINSTALL) target! Now the only dependencies left are the real ones and
      the build should be more parallelizable than before.
      
      - Be more clean in "omake clean" in support/shell.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-11 22:49:39 -0700 (Fri, 11 Jun 2004)
Revision: 5889
Log message:

      - Require omake 0.7.15
      - Minore cleanup of the refiner subdirs.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-11 23:20:58 -0700 (Fri, 11 Jun 2004)
Revision: 5890
Log message:

      Forgot to update this file as well (since it is only compiled when bytecode is used).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-12 03:17:54 -0700 (Sat, 12 Jun 2004)
Revision: 5891
Log message:

      Fixed the warning format strings.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-12 17:39:56 -0700 (Sat, 12 Jun 2004)
Revision: 5892
Log message:

      Fixed the ls problem I believe.
      Save session state.  This also saves the current directory.
      Every session has its own persistent history, etc.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-12 23:02:56 -0700 (Sat, 12 Jun 2004)
Revision: 5893
Log message:

      Added linking the inputs to lib to the .DEFAULT target.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-13 01:56:44 -0700 (Sun, 13 Jun 2004)
Revision: 5894
Log message:

      - Added a "D" (LsDocumentation) flag and a corresponding browser interface
        menu entry to be able to control whether documentation is displayed or not.
      
      - The default view flags are now
        [LsFormal; LsParent; LsRules; LsRewrites; LsDocumentation]
      
      - Now when "u" (lsUnjustified) is removed from the view flags set, the default
        flags are restored (the former "hide everything" behavior did not make much
        sense IMO).
      
      - Removed the "Interface\nbegin\n...\nend" wrapper from the theory display.
        It only waisted 3 lines and 4 columns of screen space without contributing
        anything (and was making things especially confusing when ls options
        other than "all" were used).
      
      - In prl and HTML mode, made the display of the documentation closer to
        the TeX style and less source-like. The individial display forms for some
        pieces of documentation still need work, but overall it IMHO looks OK in prl
        and pretty good in HTML.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-13 02:10:55 -0700 (Sun, 13 Jun 2004)
Revision: 5895
Log message:

      Minor HTML fixes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-13 04:28:58 -0700 (Sun, 13 Jun 2004)
Revision: 5896
Log message:

      In print_theory, use LsAll (as opposed to the "print nothing" empty set!).
      
      Note, that before the recent ls options management changes we used a custom
      selector that took care of automatically ingoring things like ML code. Now
      notghing is ignored automatically (a good thing IMHO), which means that we
      have to be more careful in placing "docoff" in all the right places.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-13 19:57:43 -0700 (Sun, 13 Jun 2004)
Revision: 5897
Log message:

      This is the new file model.
      
      Differences:
         1. Instead of "save ()", use "backup ()".
         2. Instead of "export ()", use "save ()".
         3. "backup_all ()" is called automatically when you exit.
         4. If you really want to quit without saving, use "abort ()".
         5. To revert to the last save, use "revert ()".
      
      Just to be clear, *only* the files that you have modified
      are backed-up when you quit.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-13 21:34:44 -0700 (Sun, 13 Jun 2004)
Revision: 5898
Log message:

      Fixed the problem with !restart.
      Added the commands to the File menu.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-14 09:40:18 -0700 (Mon, 14 Jun 2004)
Revision: 5899
Log message:

      These commands do not modify theories:
         expand, check, clean, squash
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-14 09:47:06 -0700 (Mon, 14 Jun 2004)
Revision: 5900
Log message:

      Be more careful about which interpret commands modify theories.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-14 11:42:12 -0700 (Mon, 14 Jun 2004)
Revision: 5901
Log message:

      Simplified the Shell.chdir function a little.
      Introduced the concept of a "mount point," to
      separate the choice of edit object from the
      chdir function.
      
      This doesn't change whether we should use real
      objects for edit objects.  However, it does suggest
      that edit objects should not handle ".." paths; that
      choice is performed by the mount handler.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-14 12:57:17 -0700 (Mon, 14 Jun 2004)
Revision: 5902
Log message:

      We had all kinds of problems with inconsistent directories in the shell.
      This uses a canonical directory name for shell_dir, fixing the consistency
      problem.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-14 13:14:39 -0700 (Mon, 14 Jun 2004)
Revision: 5903
Log message:

      Added a dummy "fs" directory.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-14 13:50:48 -0700 (Mon, 14 Jun 2004)
Revision: 5904
Log message:

      Removed edit_root, edit_up, and edit_down.  They were never used.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-15 21:10:07 -0700 (Tue, 15 Jun 2004)
Revision: 5905
Log message:

      Made sure MetaPRL compiles with THREADS_ENABLED=false.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-15 23:42:50 -0700 (Tue, 15 Jun 2004)
Revision: 5906
Log message:

      - Shell_core: minor update of some of the strings.
      - Removed Shell_root.view as it was identical to Shell_root.create.
      - status_all now needs to cd "/" at the beginning (since MetaPRL now
        starts in the original wd, not always in "/").
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-16 00:53:11 -0700 (Wed, 16 Jun 2004)
Revision: 5907
Log message:

      I thought I should commit before we get too out of date.
      This is a partial commit; I'll finish off the loose ends
      in the morning.
      
      This adds the /fs path for viewing the Unix filesystem.
      
      Notes on this commit:
         1. Removed the "view_*" functions in Shell_core.  These
            duplicated work, and were pretty pointless.
      
            However, in the browser, I see the following problem:
            the "refresh" function is not called correctly.  The symptom
            is that the display is in "prl" mode.  The solution, until
            I fix in the morning, is to call "refresh ()" explicitly.
      
         2. Use cd "/fs" to view the filesystem.  However, file editing
            with "cd" is not currently implemented; it is waiting on
            the recent discussion on "proposal for handling pwd()"
            on the onlynews@metaprl.org list.
      
         3. Shell identifiers now strings.  Sorry for this change, but
            it makes the implementation much easier.  The proper
            path is https://..../session/id1/frameset.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-16 11:56:29 -0700 (Wed, 16 Jun 2004)
Revision: 5908
Log message:

      This should fix the refresh problem.
      Tracked down a bug in restart that was jumping to the previous location
      (ouch, these are hard to find).
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-06-16 15:02:27 -0700 (Wed, 16 Jun 2004)
Revision: 5909
Log message:

      Fixed build with SSL_ENABLED on OS X.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-16 15:59:05 -0700 (Wed, 16 Jun 2004)
Revision: 5910
Log message:

      - Include -lssl/-lncurses/-lreadline only when the corresponding ENABLED
        variable is set to true.
      - access.html : the default session is now called "id1", not "1".
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-16 19:30:19 -0700 (Wed, 16 Jun 2004)
Revision: 5911
Log message:

      This is the "Newer File Model" as discussed with Aleksey.
      There are 3 levels:
         .cmoz: for auto-save versions
         .prlb: for private versions
         .prla: for public versions
      
      Commands:
         backup/backup_all: perform an auto-save (you won't normally
            need to use these)
         save/save_all: save your private copy
         export/export_all: publish your work
         revert/revert_all: revert to the last saved private version
         abort: quit MetaPRL without auto-saving (exits with an error code)
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-16 20:48:54 -0700 (Wed, 16 Jun 2004)
Revision: 5912
Log message:

      Separate "shell" sessions from "browser" sessions.
      
      Bah, browser identifiers are back to integers...  Sorry about the
      change yet again, the proper URLs are /session/%d/...
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-16 22:21:25 -0700 (Wed, 16 Jun 2004)
Revision: 5913
Log message:

      Centralized the shell handling of the "display method" data (including
      display mode, display base, display width and display destination).
      
      In partucilar:
      - The set_dfmode function now takes effect immediatelly (no need to
      cd "/";; cd "/back/where/we/were";;  after a set_dfmode).
      - The bug with "prl" mode output in "-browser" sessions seems to be gone!
      - The separation between display modes ("prl"/"src"/"html"/"tex"/"raw"/etc)
      and display "types" (i.e. destinations - Tex/Text/Browser) is now more
      complete (in fact we now _never_ convert modes into types).
      - The code for handling the display method data is no longer duplicated 5 times
      (now all code is in shell_core and proof_edit).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-16 23:36:23 -0700 (Wed, 16 Jun 2004)
Revision: 5914
Log message:

      Aleksey Nogin wrote:
      > % editor/ml/mpopt
      > Fatal error: exception Refine_error.MakeRefineError(TermType)(AddressType).RefineError("Shell_current.pid_of_string", _)
      
      Fixed.  The shell expected path of the form %s.%d.  The Shell_current
      session loader now catches the exception on garbage files, and ignores them.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-17 07:39:46 -0700 (Thu, 17 Jun 2004)
Revision: 5915
Log message:

      In DisplayTex mode, output must go to the .tex file, not stdout.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-17 08:59:13 -0700 (Thu, 17 Jun 2004)
Revision: 5916
Log message:

      Removing a bit of unused code.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-17 10:14:43 -0700 (Thu, 17 Jun 2004)
Revision: 5917
Log message:

      Removing some unused code.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-17 10:54:29 -0700 (Thu, 17 Jun 2004)
Revision: 5918
Log message:

      - Removed some more unused code.
      - Removed edit_refine (which was duplicating the edit_interpret (ProofRefine)
        functionality).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-17 12:16:29 -0700 (Thu, 17 Jun 2004)
Revision: 5919
Log message:

      Fixed the refresh problem.  The issue with refresh was that it was lazy:
      don't do a remount unless the directory has changed.  Added a force_flag
      to the chdir function.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-17 17:17:59 -0700 (Thu, 17 Jun 2004)
Revision: 5920
Log message:

      1) This makes a major change in how the relative addresses are handled
      in proof editing. Now the Proof.proof type is just a Proof.extract and
      proofs no longer keep the subaddress (relative address) internaly.
      Instead, the relative address is kept by the shell and is passed functionally
      to all the edit_* functions that need it.
      
      The only module that keeps its own copy of the relative address is Shell_fs
      (should be easy to fix, but I wanted to leave this up to Jason).
      
      Undo/Redo functions now explicitly return the new (or old, depending on
      how you look at it) relative address.
      
      2) Minor proof updates in itt_list2
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-17 17:55:21 -0700 (Thu, 17 Jun 2004)
Revision: 5921
Log message:

      Inlined the access.js back into access.html. This is necessary because
      the /input/... URLs do not get "%%RESPONSE%%" substitution performed.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-06-17 18:00:57 -0700 (Thu, 17 Jun 2004)
Revision: 5922
Log message:

      Removed access.js
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-17 18:02:53 -0700 (Thu, 17 Jun 2004)
Revision: 5923
Log message:

      Oops, one more place with access.js
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-17 18:15:11 -0700 (Thu, 17 Jun 2004)
Revision: 5924
Log message:

      Added file support.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-06-17 18:46:39 -0700 (Thu, 17 Jun 2004)
Revision: 5925
Log message:

      Corrected OS X docs.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-17 18:56:36 -0700 (Thu, 17 Jun 2004)
Revision: 5926
Log message:

      - Fixed (hopefully) the source mode display forms for variables.
      - When turning variable names into name+subscripts, only split off numbers,
      but not letters.
      - Fixing a bug in Shell_rule.edit_check_addr - [] should be always accepted.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-17 19:07:40 -0700 (Thu, 17 Jun 2004)
Revision: 5927
Log message:

      Added some extra items to the menus.
      Note, I need to work on disabling them
      when outside of a proof.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-17 19:24:43 -0700 (Thu, 17 Jun 2004)
Revision: 5928
Log message:

      Update so styles work in IE too.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-17 21:09:57 -0700 (Thu, 17 Jun 2004)
Revision: 5929
Log message:

      - Made the definitions viewable
      - More "src" mode dform fixes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-17 22:02:50 -0700 (Thu, 17 Jun 2004)
Revision: 5930
Log message:

      A few display form fixes:
      - directory and file listings should use newline, not hspace
      - proof node display needs to put goal/subgoal/assumption/etc terms in a slot.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-17 22:10:14 -0700 (Thu, 17 Jun 2004)
Revision: 5931
Log message:

      Cd to the MetaPRL root before running CVS.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-17 22:44:31 -0700 (Thu, 17 Jun 2004)
Revision: 5932
Log message:

      - The "/manual/filename" URIs now serve the documentation from the
        doc/htmlman directory in the local MetaPRL installation.
      - Added a bit of content to the MetaPRL welcome page.
      - The body page should not reset the hostname to the default value.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-17 23:15:32 -0700 (Thu, 17 Jun 2004)
Revision: 5933
Log message:

      Added MetaPRL version to the Welcome page. HTML could be nicer, though.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-17 23:21:52 -0700 (Thu, 17 Jun 2004)
Revision: 5934
Log message:

      Adding the .ico version of the metaprl.png file.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-17 23:32:00 -0700 (Thu, 17 Jun 2004)
Revision: 5935
Log message:

      Adding the MetaPRL "shortcut" icon (both Mozilla and IE should be happy, hopefully).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-17 23:42:58 -0700 (Thu, 17 Jun 2004)
Revision: 5936
Log message:

      Emphasize the "Start" link.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-18 08:43:37 -0700 (Fri, 18 Jun 2004)
Revision: 5937
Log message:

      I tried to move the display forms to Shell_fs, but it didn't work,
      so I moved it back.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-18 09:44:45 -0700 (Fri, 18 Jun 2004)
Revision: 5938
Log message:

      Re-introduced fs_cwd.  Handle pathnames appropriately in Shell_syscall.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-18 11:02:14 -0700 (Fri, 18 Jun 2004)
Revision: 5939
Log message:

      Re-use the HTTP socket on a restart.  The socket descriptor
      and challenge are saved in the environment.  So this means
      it won't work on Windows, where sockets do not have integer
      descriptors.  Have to think about how to do that, or else
      just disable the feature on Windows.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-18 11:09:37 -0700 (Fri, 18 Jun 2004)
Revision: 5940
Log message:

      Add the session and directory to the title bar.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-18 11:41:43 -0700 (Fri, 18 Jun 2004)
Revision: 5941
Log message:

      - Forgot the tex mode yesterday. Jason, does your new "src is a special mode"
      functionality provide some way to specify "really all modes" w/o resorting to
      "mode[src] :: mode[prl] :: mode[html] :: mode[tex]"?
      
      - Added a missing docoff
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-18 14:38:45 -0700 (Fri, 18 Jun 2004)
Revision: 5942
Log message:

      This is probably the final round of changes.
      All windows are internal now.
      Coming in in about 30min.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-18 16:04:33 -0700 (Fri, 18 Jun 2004)
Revision: 5943
Log message:

      - Do not die on entering a primitive item (is_edit_enabled needed to return
      false right away, without trying to go through Proof_edit in that case).
      
      - Proof_info needs to write .cmoz using a "non-interactive" magic (to allow
      the compiler to overwrite them). Note that the flags are maintained
      imperatively, so the whole setup ends up being a big hack. :-(
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-18 17:40:26 -0700 (Fri, 18 Jun 2004)
Revision: 5944
Log message:

      An alternative fix to the "InteractiveSummary" problem, hopefully this time
      it will work.
      
      Package_info would now always set the InteractiveSummary flag (which is
      a correct thing to do). And Filter_parse will now force saving to .cmoz
      (not just to "first available"), which is a good thing and will force
      the InteractiveSummary flag as well (a bit of a hack, but oh well).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-18 18:35:03 -0700 (Fri, 18 Jun 2004)
Revision: 5945
Log message:

      support/shell/session_io.ml is a generated file and needs to be cleaned.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-18 18:45:06 -0700 (Fri, 18 Jun 2004)
Revision: 5946
Log message:

      Added "fs" module to root.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-18 19:25:01 -0700 (Fri, 18 Jun 2004)
Revision: 5947
Log message:

      Added a build-time framework for groupping MetaPRL modules into theories.
      Still need to modify the shell code to make use of this information.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-18 21:03:40 -0700 (Fri, 18 Jun 2004)
Revision: 5948
Log message:

      Moved the Shell.command struct outside of the shell, so that we can
      use these commands in other modules.
      
      Someday we should think about moving Shell_mp and Shell_p4 into the
      shell/support directory so we can avoid this imperative nonsense.
      One thing to consider, we can abandon Shell_p4 entirely.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-19 12:51:11 -0700 (Sat, 19 Jun 2004)
Revision: 5949
Log message:

      Since basic shell commands no longer live in Shell, the theories that used
      to "extends Shell" now need to "extand Shell_theory" (or Shell_commands).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-19 15:08:10 -0700 (Sat, 19 Jun 2004)
Revision: 5950
Log message:

      By default (i.e. when outside of a package), use Shell_theory display forms,
      not just the Summary ones.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-19 15:39:37 -0700 (Sat, 19 Jun 2004)
Revision: 5951
Log message:

      Output is persistent.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-19 16:01:14 -0700 (Sat, 19 Jun 2004)
Revision: 5952
Log message:

      Moved file display forms from Summary to Shell_fs.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-19 16:15:07 -0700 (Sat, 19 Jun 2004)
Revision: 5953
Log message:

      If refresh fails (the module or directory might no longer exist), try falling
      back to empty relative dir and if that does not work, fall back to DirRoot.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-19 16:49:18 -0700 (Sat, 19 Jun 2004)
Revision: 5954
Log message:

      1) Group the modules into theories. Now the filesystem structure has the
      following form: "/group/module/rule/nn/nn/nn/..."
      
      Note that "old-style" locations are still valid - any attempt to go to
      "/module/..." would result in getting to "/group/module/..." for the group
      that the module resides in (but weird things might happen if a group name
      clashes with a module name :-(, so do not do that).
      
      The group name and description are specified using THEORYNAME and THEORYDESC
      variables in [O]Makefile.
      
      2) I've added an "end" anchor to the end of the messages frame, so hopefully
      it will keep scrolling to the right place.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-19 20:46:59 -0700 (Sat, 19 Jun 2004)
Revision: 5955
Log message:

      Fixed the problem with going to some random directory on restart.
      
      Note:
         Mozilla tries to remember subframe locations on location.reload();
         To avoid this, use location.href = location.href.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-19 22:09:03 -0700 (Sat, 19 Jun 2004)
Revision: 5956
Log message:

      - The Lm_big_int.of_string had no support for non-decimal formats (0xN, 0bN,
        etc) and no sanity checking (for example, "0x" was interpreted as 72!). I
        made Lm_big_int.of_string to act the same way as Pervasives.int_of_string.
      
      - I changed the way long arrows are translated to HTML in an attept to make
        then actually be long. Please verify under IE and other browsers!
      
      - The extract term (for primiteve rules) needs to be in a slot.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-20 08:54:04 -0700 (Sun, 20 Jun 2004)
Revision: 5957
Log message:

      Fixed Javascript string escapes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-20 15:05:31 -0700 (Sun, 20 Jun 2004)
Revision: 5958
Log message:

      Added 3 new is_enabled methods - MethodRedo (checks whether redo stack is empty),
      MethodExpand (tells whether we are in a proof and the current proof not is not
      yet expanded), and MethodApplyAll (tells whether we are in a place where *_all -
      expand_all, status_all and check_all - whould make sense).
      
      For now, I pnly updated the Edit -> Redo item to use the new MethodRedo (instead
      of MethodUndo); the other two are unused.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-20 15:45:34 -0700 (Sun, 20 Jun 2004)
Revision: 5959
Log message:

      Changed apply_all to do the right thing in case it is called inside
      a "/group" directory. Also, added a bit of sanity checking to it
      (so now apply_all would fail when inside of a proof as opposed to
      suddenly applying things to the whole package).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-20 17:26:43 -0700 (Sun, 20 Jun 2004)
Revision: 5960
Log message:

      Made editing much more robust, so that you don't lost work
      on a restart.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-20 18:35:32 -0700 (Sun, 20 Jun 2004)
Revision: 5961
Log message:

      The init function is now in Shell_current.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-20 20:40:44 -0700 (Sun, 20 Jun 2004)
Revision: 5962
Log message:

      Fixed some browser problems with IE.
      Note: you can now use line numbers when editing files.
      This update was performed using the browser interface.
      

Changes by: ( at unknown.email)
Date: 2004-06-20 20:40:44 -0700 (Sun, 20 Jun 2004)
Revision: 5963
Log message:

      This commit was manufactured by cvs2svn to create branch
      'unlabeled-1.23.2'.

Changes by: ( at unknown.email)
Date: 2004-06-20 20:40:44 -0700 (Sun, 20 Jun 2004)
Revision: 5964
Log message:

      This commit was manufactured by cvs2svn to create branch
      'unlabeled-1.7.2'.