/[mojave]/metaprl/editor/ml/shell.ml
ViewVC logotype

Log of /metaprl/editor/ml/shell.ml

Parent Directory Parent Directory | Revision Log Revision Log


Sticky Revision:
(Current path doesn't exist after revision 4545)

Revision 3584 - (view) (download) (annotate) - [select for diffs]
Modified Thu Apr 25 15:28:40 2002 UTC (19 years, 2 months ago) by nogin
File length: 52849 byte(s)
Diff to previous 3444
- Added the comment module to the theories.pdf ("make latex").

- Added a hack allowing to override a theory display with another theory's
display. This is necessary for bootstrapping reasons - it allows one
to get a reasonable output of a theory (e.g. Comment) that is defined before
all essential display forms (e.g. the Summary ones) are there.

- Added debugging code to make it easier to find dforms that cause
zone begin/end mismatch (and used it to get rid of all
the "Unballanced buffer" warnings in "make latex").

- Minor dforms&comments updates.


Revision 3444 - (view) (download) (annotate) - [select for diffs]
Modified Thu Nov 15 23:03:47 2001 UTC (19 years, 7 months ago) by nogin
File length: 52797 byte(s)
Diff to previous 3322
Code cleanup:

I looked (using the code I've put into macro.ml) for places where the same code
appeared in several branches of a match or function expression. I changed those
places to use a complex pattern and a single copy of the code.


Revision 3322 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jul 8 16:12:09 2001 UTC (19 years, 11 months ago) by nogin
File length: 52965 byte(s)
Diff to previous 3276
Use String.concat instead of String_util.concat


Revision 3276 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jun 19 15:17:10 2001 UTC (20 years ago) by nogin
File length: 52970 byte(s)
Diff to previous 3268
Added support for the following syntax of resource improvement:
let resource name += expr
and
let resource name += [ expr1; expr2; ...; exprn ]


Revision 3268 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 15 23:16:03 2001 UTC (20 years ago) by nogin
File length: 52807 byte(s)
Diff to previous 3267
Implemented object status inquiry:
 status ();;
   -- tells the status of the current object
 status_all ();;
   -- re-runs all proofs in the current node and tells their status
   -- from root - same for all the proofs in MetaPRL


Revision 3267 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 15 20:35:54 2001 UTC (20 years ago) by nogin
File length: 51227 byte(s)
Diff to previous 3240
expand_all() should go to next item on any exception, not just
RefineError.


Revision 3240 - (view) (download) (annotate) - [select for diffs]
Modified Mon May 28 22:16:27 2001 UTC (20 years ago) by nogin
File length: 51239 byte(s)
Diff to previous 3079
Use terminal width for output in a more consistent manner.


Revision 3079 - (view) (download) (annotate) - [select for diffs]
Modified Tue Sep 26 00:09:12 2000 UTC (20 years, 8 months ago) by nogin
File length: 51291 byte(s)
Diff to previous 3076
The result of MP toploop expression evaluation is now also formatted
using the terminal width. Also, tuples and lists should be now formatted nicer
in toploop.


Revision 3076 - (view) (download) (annotate) - [select for diffs]
Modified Sun Sep 24 01:42:22 2000 UTC (20 years, 9 months ago) by jyh
File length: 51376 byte(s)
Diff to previous 3057
Oops, that last checkin had a bug: I forgot about the correct
ordering of fields in a union.  There are separate numbering orders
for constants and for fields with values.


Revision 3057 - (view) (download) (annotate) - [select for diffs]
Modified Sun Sep 10 18:26:37 2000 UTC (20 years, 9 months ago) by jyh
File length: 51324 byte(s)
Diff to previous 3048
This jumbo update is a documentation update.  There are no
logical changes.  I did two things:

1. First, comments that begin with the sequence "(*!" are
   interpreted as structured comments.  The contents are parsed
   as terms, and the comments will display in the editor window.
   The comments may contain arbitrary text, as usual, and they
   can also contain explicit terms.  The syntax for terms is:

   @opname[p1, ..., pn]{t1; ...; tm}

   or there is an alternate syntax:

   @begin[opname, p1, ..., pn]
   arg
   @end[opname]

   Text sequences count as a single term.  So, for instance, the
   term @bf{Hello world} display the "Hello world" text in a bold
   font.

   The "doc" term is used for text that is considered to be
   documentation.  There is a set of LaTeX-like terms that you can
   use to produce good-looking documentation.  These are all
   documented in the theories/tactic/comment.ml module.  The exact
   syntax of structured comments is defined in the
   mllib/comment_parse.mll file.  You can also look at any of the
   module in the theories/itt directory if you want to see examples.

   You can generate a pritable version of documentation with the
   print_theory command in the editor.  For example, the command

   # print_theory "itt_equal";;

   produces a file called output.tex that can be formatted with
   your favorite version of latex2e.  You can also generate a
   manule of all the theories by running "make tex" in the
   editor/ml directory.  Or you can run "make" in the
   doc/latex/theories directory.

   The files are hyperlinked, and they contain a table of contents
   and an index.  The preferred reader is acrobat, and the preferred
   formatter is pdflatex.

2. Second, I documented the tactic, base, itt, and czf theories.

3. Oh, and I also added a spelling checker:)  You can turn on the
   spelling checker with the -debug spell option or MP_DEBUG=spell.
   If prlc thinks that your files contain spelling mistakes, it will
   print them out and abort.  You can fix this problem by 1) fixing
   the spelling error, 2) adding the words withing a @spelling{words}
   term in a comment, or adding the words to you .ispell_english
   directory.

   For example, we could either do this:

   @begin[spelling]
   Aleksey Nogin
   @end[spelling]

   Or we could just add Alexey to either $cwd/.ispell_english, or
   ~/.ispell_english.

   The spell checker uses /usr/dict/words as a database, which it
   compiles to a hashtable in /tmp/metaprl-spell-$USER.dat.  Don't
   worry about the tmp file, it is generated automatically.


Revision 3048 - (view) (download) (annotate) - [select for diffs]
Modified Wed Aug 16 07:29:04 2000 UTC (20 years, 10 months ago) by nogin
File length: 50920 byte(s)
Diff to previous 3036
Fixed some mess with dispaly forms. But we still need to implement mode generality,
sets of modes (or at least something like mode[all except src] flag)
and make sure that the modes are correct on all the dforms.


Revision 3036 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jul 27 19:55:54 2000 UTC (20 years, 10 months ago) by nogin
File length: 50908 byte(s)
Diff to previous 3024
- Fixed the problem with leaking attributes.

- Fixed the problem with top-level functions (such as clean_all)
removing the "Primivive" flag and replacing it with "Interactive".

- Fixed some display forms.

- Removed "empty" .prla files in ITT and "refreshed" the rest of them.

- More in BUGS and TODO.

- Other small changes.


Revision 3024 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jul 12 06:30:51 2000 UTC (20 years, 11 months ago) by nogin
File length: 50711 byte(s)
Diff to previous 3023
- Do not forget to reset the proof item address before leaving the item.
- Debugging exhancement and small bugfixes in proof_boot.


Revision 3023 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jul 11 05:04:33 2000 UTC (20 years, 11 months ago) by nogin
File length: 50612 byte(s)
Diff to previous 2986
Additional debugging.


Revision 2986 - (view) (download) (annotate) - [select for diffs]
Modified Thu May 25 22:29:55 2000 UTC (21 years, 1 month ago) by nogin
File length: 50258 byte(s)
Diff to previous 2985
Splitted create_tptp into create_ax_statement and tptp_load.

Now editor/ml/ does not refer to Tptp_load which we had to comment and uncomment
all the time.


Revision 2985 - (view) (download) (annotate) - [select for diffs]
Modified Thu May 25 05:14:42 2000 UTC (21 years, 1 month ago) by nogin
File length: 50251 byte(s)
Diff to previous 2922
Merged the unify_mm branch.


Revision 2922 - (view) (download) (annotate) - [select for diffs]
Modified Thu Mar 16 19:52:02 2000 UTC (21 years, 3 months ago) by lolorigo
File length: 50262 byte(s)
Diff to previous 2912
added/improved functionality for metaprl/jprover/nuprl5 io


Revision 2912 - (view) (download) (annotate) - [select for diffs]
Modified Thu Feb 24 06:55:47 2000 UTC (21 years, 4 months ago) by jyh
File length: 50251 byte(s)
Diff to previous 2906
Most of the theories in Itt now expand without errors.
One exception is Itt_fset, which will require some work.


Revision 2906 - (view) (download) (annotate) - [select for diffs]
Modified Tue Feb 22 17:42:16 2000 UTC (21 years, 4 months ago) by jyh
File length: 49876 byte(s)
Diff to previous 2886
Itt_bool now expands.


Revision 2886 - (view) (download) (annotate) - [select for diffs]
Modified Thu Feb 17 22:44:34 2000 UTC (21 years, 4 months ago) by nogin
File length: 49774 byte(s)
Diff to previous 2884
Now ``cd "/theory"'' also initializes the theory, so there is no need
to do ``ls ""'' before being able to type in terms and use the theory.

P.S. There is probably a better way to this, so I marked it as HACK.


Revision 2884 - (view) (download) (annotate) - [select for diffs]
Modified Thu Feb 17 22:05:25 2000 UTC (21 years, 4 months ago) by nogin
File length: 49615 byte(s)
Diff to previous 2857
Now z.ml runs again


Revision 2857 - (view) (download) (annotate) - [select for diffs]
Modified Sun Nov 21 22:19:12 1999 UTC (21 years, 7 months ago) by nogin
File length: 49507 byte(s)
Diff to previous 2822
BUG 2.3 now includes:

Loading the same theory twice produces similar problems.

As a result, `load'ing a theory and then `cd'ing into it
(which attempts to load the theory again) does not quite work.
As a temporary workaround, the "load" function was removed from
toploop.


Revision 2822 - (view) (download) (annotate) - [select for diffs]
Modified Fri Oct 22 01:07:59 1999 UTC (21 years, 8 months ago) by nogin
File length: 49262 byte(s)
Diff to previous 2808
Added new function to mp_debug
let show_loading s = if !debug_load then Printf.eprintf s eflush

and replaced all usages of debug_load with show_loading


Revision 2808 - (view) (download) (annotate) - [select for diffs]
Modified Wed Aug 25 19:09:25 1999 UTC (21 years, 10 months ago) by jyh
File length: 49321 byte(s)
Diff to previous 2786
I added a TeX mode for display.  This was a quick hack, and it
it _not_ the way it should be done long term.  We should be able
to do the formatting and indentation with boxes, etc.

I added SIL.  This theory is an incomplete semantics of a
"simple imperative language."


Revision 2786 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jul 5 13:38:57 1999 UTC (21 years, 11 months ago) by jyh
File length: 49061 byte(s)
Diff to previous 2775
Added: Itt_logic.genAssumT : int list -> tactic
This tactical "generalizes" over a set of assumptions.  The first
assumption should be for a membership judgment.  For example:
   ...
i. H >- t in T list
   ...
j. H >- Q[t]
   ...
   H >- P[t]
   BY genAssumT [i; j]
1. H >- all l: T list. (Q[l] => P[l])
2. H; x: (all l: T list. (Q[l] => P[l])) >- P[t]


Revision 2775 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jul 4 13:13:44 1999 UTC (21 years, 11 months ago) by jyh
File length: 48932 byte(s)
Diff to previous 2753
Things seem to be working pretty smoothly now.  This is mostly minor
fixes.  Still need to fix the problems with the mp toploop.

    1. Proofs now use Alexey's ASCII format.  By default, proofs
       should be saved to CVS in .prla format.  You can generate ASCII
       files by using "make export", or you can use the "export ()"
       instead of the "save ()" command in the editor.  For speed,
       .prlb files are now saved in a raw, marshaled format.  When you
       edit a theory, the newest of .cmoz, .prlb, or .prla files is
       loaded.  There is a new command "convert" to convert between
       all the different proof file formats.
          convert -I ... [-raw|-term|-lib|-ascii] -impl file.cmoz
          raw: save the file in fast, raw format
	  term: save the file as <magic#>/<marshaled term_io>
	  lib: send the file to the Nuprl5 library
	  ascii: create a .prla file

       Developers: _please_ mention any changes to the basic data
          structures in your CVS logs.  The things that matter are:
          Refiner.Refiner.TermType.term
	  Filter_summary.summary_info
	  Tactic_boot_sig.TacticType.{tactic_arg,extract}
	  Proof_boot.io_proof

       Users: to be safe, save all your proofs using "make export"
          before doing a cvs update.

    2. "expand ()" and "expand_all ()" now work.  I also added
       "clean ()" and "clean_all ()" commands to remove those peasky
       dangling proof nodes when you are satisfied with a proof.  By
       default, proofs are saved only down to the innermost rule-box
       level, and primitive refinements are omitted.  I haven't added
       a "deep_save ()" command; it seems unecessary.

    3. Sorry, but I had to move theories/boot into the filter.  There
       are no major changes here, but the directory structure in
       filter has changed significantly.

    4. I added a THEORIES variable to the mk/config file that
       specifies what theories you want to compile.  This means that
       you don't have to edit all the Makefiles when you add a theory,
       and it also means that you can keep your own theories without
       having to commit them to cvs.


Revision 2753 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 25 00:19:15 1999 UTC (22 years ago) by jyh
File length: 47831 byte(s)
Diff to previous 2743
These are some minor changes to make things work better.  Changed
meaning of ThinOption in elim_resource: it now means to thin the hyp
by default, unless overridden by thinningT false.

Fixed some proof operations.  Added "move_to_assum" command to take
the current subgoal and make it an extra assumption of the entire
proof (it may not work at the moment).

ls now takes a _string_ argument.  Use ls "u";; to display only the
unproved rules in the current module.

Proved many membership variants of the standard type constructors,
but there are a few more to go.  When you are defining theories, I
believe you should use membership, not equality.  After all, equality
is derivable from membership, and membership is a lot easier.

Still to go: ASCII format proof files; save proofs _without_ extracts
by default.  The expand () function does not reexpand proofs correctly.
A few problems with proof navigation.


Revision 2743 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 23 04:50:29 1999 UTC (22 years ago) by jyh
File length: 46336 byte(s)
Diff to previous 2668
This is a major release; I bumped the release number to 0.6.
WARNING: There are major changes here, and there may be problems
   with this version that prevent you from using your old proof.
   Save your work before using this version.
NOTE: If you decide to try this out, and you find problems,
   please(!) send me email so I can fix it.

Changes:
   1. The proof structure is totally changed, so that the proof
      editor edits the raw proof extracts.  This means that you
      can view the actions of the refiner down to the primitive
      rule applications.  In the proof editor, you can use
      "down 0" (or "cd "0") to descend into the proof of a rule box.
      Primitive proofs are called "extracts", and are labeled with
      brackets (like [extract]).  To expand the extract, use the command
      "unfold ()".  You should be able to get all the way down to
      the primitive rule/rewrite applications.

      This also means that the format of the proof files (the .prlb
      files) has changed.  The old proof files are still valid,
      but this is a hack and will be deprecated in the next
      few months.  I haven't yet added Alexey's ASCII proof
      files, but that will come with the next release.

      As usual, the "undo ()" command undoes the last proof step,
      including "unfold ()".  The "nop ()" command, reset the undo
      stack.  I also added a "redo ()" command that undoes the
      last undo.

      There is a simple rule-box proof cache for collecting proofs
      as you edit them.  If cached proofs are available, you will
      see them in brackets (like [* # * *]) on the status line.
      I haven't yet:( added the commands to use cached proofs.

   2. Refiner changes.  I added two new features: the "cutT <term>"
      tactic cuts in a new assumption.  Also, you can apply
      rewrites directly on assumptions, with the "rwc" and
      "rwch" operations, that take a clause argument.  Basically,
      this means that instead of folding the goal, you can unfold
      the assumption.  I believe this is sound; let me know if
      you think otherwise!

   3. Resource changes.  I added resource automation, built on
      the basic resource parsing Alexey added.  Ratherthan writing
      resource code for every rule, you can annotate most rules
      to generate the resource code directly.  You can see lots of
      examples in the Itt theory.  Basically, there are three useful
      resources annotations:
         intro_resource []: adds the rule as an introduction in dT
         intro_resource [SelectOption i]: adds to selT i dT
         elim_resource []: adds as an elimination rule to dT.
            This normally tries to thin the hyp that was eliminated.
         elim_resource [ThinOption]: don't thin the hyp

      Rules should be annotated with labels on their clauses,
      like [wf], [main], [assertion], etc.  This means that in
      most tactic aplcations, you no longer need to have the
      thenLT [addHiddenLabel "main"; ...] part.

      N.B.  This is the most likey parts of this release to
      cause problems, because I deleted most old resource code.

      Also, you can still write standard resource code, but there
      is no longer a d_resource--it has been broken into two parts:
      the intro_resource for application to goals, and elim_resource
      for application to hyps.

   4. The proof editor is multi-threaded, so you can work on multiple
      proofs simultaneously.  In the normal Emacs editor, this is
      no help for you.  But there is a new Java editor with the
      standard point-and-click interface, and it views the proof
      in HTML, with multiple windows etc.  The beautiful thing is
      that you can use display forms to add commands to edit windows.
      The sad thing is that I built it on NT, Java 1.2 is required,
      and I haven't tried the blackdown.org Java release on Linux.
      This editor is pending some bug fixes from Sun to get the
      fonts right (they call this a standard release?).

      In any case, here are the direct implications.  The display
      forms have an "html" mode.  The display form formatting in
      the module Rformat has been completely redone, but display
      _should_ be the same as it was before.

      It is likely that I will add an HTML dump, so we can send
      uneditable proofs around by email or on the web.  Check out
      the file theories/base/summary.ml to see some example HTML
      display forms.

      The other issue: your MetaPRL process starts a web server on
      YOUR local machine using YOUR process id on the "next" available
      TCP port, and it serves files only from the search path that you pass
      MetaPRL.  I realize that this has security implications.  This
      is necessary to get browser access to the working MetaPRL proof.
      Is this crazy?  Let me know your beliefs, religious or
      otherwise.

   5. There are numerous minor changes.  I redid parts of the WeakMemo,
      Term_header_constr, and TermHash.  The theories/tactic directory
      has been split into tactic/boot (which is not compiled by MetaPRL),
      and theories/tactic (which is).

Jason


Revision 2668 - (view) (download) (annotate) - [select for diffs]
Modified Sun May 23 00:00:51 1999 UTC (22 years, 1 month ago) by jyh
File length: 38684 byte(s)
Diff to previous 2652
Added ML side-conditions, so that rewrites and rules can be defined
with ML code in the really necessary cases.  The ml_rw keyword
declares/defines an ML rewrite, and ml_rule declares/defines
an rule application defined in ML.


Revision 2652 - (view) (download) (annotate) - [select for diffs]
Modified Thu May 13 23:18:29 1999 UTC (22 years, 1 month ago) by kopylov
File length: 38681 byte(s)
Diff to previous 2638
1) Added a bug list into BUGS

2) Changed the keywords:
axiom -> rule  (.mli files)
primrw -> prim_rw  (.ml files)
rwthm -> thm_rw  (.ml files)

3) Fixed the rule Itt_struct.hypSubstitution


Revision 2638 - (view) (download) (annotate) - [select for diffs]
Modified Thu Apr 8 01:33:12 1999 UTC (22 years, 2 months ago) by nogin
File length: 38689 byte(s)
Diff to previous 2604
Moved most filter_summary types into the filter_type.mlz


Revision 2604 - (view) (download) (annotate) - [select for diffs]
Modified Thu Mar 4 15:02:04 1999 UTC (22 years, 3 months ago) by lolorigo
File length: 38672 byte(s)
Diff to previous 2600
Implemented access to rewrites and fixed saving of theories in nuprl/mp link


Revision 2600 - (view) (download) (annotate) - [select for diffs]
Modified Wed Feb 24 23:26:23 1999 UTC (22 years, 3 months ago) by nogin
File length: 36960 byte(s)
Diff to previous 2577
Added print_gc_stats: unit -> unit command to the toploop.


Revision 2577 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jan 28 18:44:05 1999 UTC (22 years, 4 months ago) by jyh
File length: 36872 byte(s)
Diff to previous 2575
Upgraded to OCaml 2.01.


Revision 2575 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jan 25 19:23:08 1999 UTC (22 years, 4 months ago) by jyh
File length: 36757 byte(s)
Diff to previous 2574
Added edit_save function to save a specific package.


Revision 2574 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jan 25 18:34:13 1999 UTC (22 years, 4 months ago) by jyh
File length: 36666 byte(s)
Diff to previous 2553
Added edit_set_goal, which loads the package if it is not yet loaded.


Revision 2553 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jan 3 05:31:04 1999 UTC (22 years, 5 months ago) by nogin
File length: 36080 byte(s)
Diff to previous 2549
Added profiling control functions stop_gmon and restart_gmon to MP
top loop. Now it is possible to get a "clean" profiling information
that does not include any startup overhead.


Revision 2549 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jan 1 20:14:13 1999 UTC (22 years, 5 months ago) by jyh
File length: 35814 byte(s)
Diff to previous 2538
Fixed up "make clean" to remove more files.
The directory should be like a new checkout afterwards.
Enabled set_debug function in toploop.  You can
turn on debugging with

# set_debug "xxx" true;;

for some debug variable xxx.


Revision 2538 - (view) (download) (annotate) - [select for diffs]
Modified Thu Dec 31 17:23:10 1998 UTC (22 years, 5 months ago) by jyh
File length: 35710 byte(s)
Diff to previous 2528
Added module-checking function "expand_all" to the Shell module.


Revision 2528 - (view) (download) (annotate) - [select for diffs]
Modified Tue Dec 29 20:14:09 1998 UTC (22 years, 5 months ago) by jyh
File length: 32736 byte(s)
Diff to previous 2527
Added "kreitz" command to fold up an entire proof subtree into a single node.


Revision 2527 - (view) (download) (annotate) - [select for diffs]
Modified Tue Dec 29 19:11:40 1998 UTC (22 years, 5 months ago) by jyh
File length: 32504 byte(s)
Diff to previous 2525
Proof expansion works.
Fixed a bad typo in red_black_set.


Revision 2525 - (view) (download) (annotate) - [select for diffs]
Modified Mon Dec 28 21:07:52 1998 UTC (22 years, 5 months ago) by jyh
File length: 31880 byte(s)
Diff to previous 2494
Numerous minor changes.

Added itt_fset: a theory of finite sets based on a list
implementation quotiented by equivalence under arbitrary
occurrences and ordering.

Added initial reflection theory.  Terms are quotiented by
alpha-equality, so normal well-formedness proofs are difficult,
and more work needs to be done to define free variables and
substitution.


Revision 2494 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 13 01:14:08 1998 UTC (22 years, 8 months ago) by jyh
File length: 31882 byte(s)
Diff to previous 2491
I changed all the obvious places of Nuprl-Light, NL, nl, or any
other instance to MetaPRL, MP, or mp, etc.  The docs may be broken
but I'll fix them soon.  As usual, let me know if anything breaks.


Revision 2491 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 6 19:54:12 1998 UTC (22 years, 8 months ago) by jyh
File length: 31886 byte(s)
Diff to previous 2490
Added the display form functions for Nuprl5.


Revision 2490 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 6 14:08:25 1998 UTC (22 years, 8 months ago) by jyh
File length: 28395 byte(s)
Diff to previous 2486
Added evaluation functions to ShellP4.
Lori: the "open" functions do not work in edit_cd_thm.  I believe
that the "open" expresssions are evaluated in a separate toploop,
so there is no way to open the module in the real toploop
except by typing it in...


Revision 2486 - (view) (download) (annotate) - [select for diffs]
Modified Mon Oct 5 15:56:29 1998 UTC (22 years, 8 months ago) by jyh
File length: 28016 byte(s)
Diff to previous 2482
Modified Shell.edit_create_thm _not_ to take an initial sequent.


Revision 2482 - (view) (download) (annotate) - [select for diffs]
Modified Wed Sep 30 01:34:37 1998 UTC (22 years, 8 months ago) by eli
File length: 28193 byte(s)
Diff to previous 2477
cd is now used for all navigations, for example:
  cd "/test/test1/1/2"
goes to the second subgoal of the first of the test1 theorem.
  cd ".."
is the same as up 1 (which now uses cd).
  cd "..."
is equivalent to cd "../..".
Note: Path `normalization' is done before processing, so cd "X/.." always work.


Revision 2477 - (view) (download) (annotate) - [select for diffs]
Modified Tue Sep 29 00:33:29 1998 UTC (22 years, 8 months ago) by jyh
File length: 26820 byte(s)
Diff to previous 2473
Added some features Lori requested for the Nuprl5 editor, plus
a syntax fix in the Fol_implies module.


Revision 2473 - (view) (download) (annotate) - [select for diffs]
Modified Wed Sep 23 20:34:33 1998 UTC (22 years, 9 months ago) by jyh
File length: 26755 byte(s)
Diff to previous 2472
Fixed loading in edit_list_module.


Revision 2472 - (view) (download) (annotate) - [select for diffs]
Modified Wed Sep 23 18:58:50 1998 UTC (22 years, 9 months ago) by jyh
File length: 26692 byte(s)
Diff to previous 2465
Removed bogus quotes from edit_cd_thm.


Revision 2465 - (view) (download) (annotate) - [select for diffs]
Modified Fri Sep 11 20:23:54 1998 UTC (22 years, 9 months ago) by jyh
File length: 26695 byte(s)
Diff to previous 2456
Added Nuprl5 interface to editor/ml/shell.mli


Revision 2456 - (view) (download) (annotate) - [select for diffs]
Modified Sat Sep 5 22:31:37 1998 UTC (22 years, 9 months ago) by jyh
File length: 23693 byte(s)
Diff to previous 2442
Added license headers to each of the files in preparation for
the first major release.  The license is GNU public license; if
any of you have problems with that, let me know right away.  When
you add new code, you should credit yourself as the author.  When
you modify code, you should add a "Modified by:" to the header,
and possibly a short summary of your changes.

I tried to get the Author lists as correct as I remember, but there
are more than 550 files(!) and I may have made some mistakes. Please
add yourself if I didn't do it right.


Revision 2442 - (view) (download) (annotate) - [select for diffs]
Modified Fri Aug 21 22:22:55 1998 UTC (22 years, 10 months ago) by jyh
File length: 22534 byte(s)
Diff to previous 2441
Added distributed refinement using Ensemble.
This is an initial version.  The scheduler needs some performance
tuning, and Ensemble needs a little work on blocking IO.

By default, Ensemble support is not compiled into Nuprl-Light.
To enable distributed refinement, you need a copy of Ensemble,
which is available at:

    http://www.cs.cornell.edu/Info/Projects/Ensemble/

When Ensemble is installed, set the environment variable
ENSROOT to the root Ensemble directory.  On mojave, I've precompiled
a version of Ensemble in ~jyh/nuprl/src/ensemble.  Once this
variable is set, make will build the distributed refiner.

Ensemble uses a separate "gossip" daemon to get processes to form groups.
The program editor/ml/nlgossip starts this daemon.  Once the daemon
is started, multiple copies of nl will know about each other, and ship
refinement jobs to each other.  So if you want faster refinement, start
multiple copies of nl.  These copies can be started and killed at
any time; Ensemble provides support for failure detection and recovery.


Revision 2441 - (view) (download) (annotate) - [select for diffs]
Modified Tue Aug 18 02:31:31 1998 UTC (22 years, 10 months ago) by eli
File length: 22638 byte(s)
Diff to previous 2407
Changed the `directory' separator from "." to "/";
cd changes info.dir only after possible errors.


Revision 2407 - (view) (download) (annotate) - [select for diffs]
Modified Wed Aug 5 01:12:22 1998 UTC (22 years, 10 months ago) by jyh
File length: 22161 byte(s)
Diff to previous 2388
Added util String_set module.
Unification now used String_set.StringSet for the constants (Term_ds
still uses its own StringSet).
Modified sequent display.
Added Shell.goal () to the the current proof goal.


Revision 2388 - (view) (download) (annotate) - [select for diffs]
Modified Sun Aug 2 21:36:26 1998 UTC (22 years, 10 months ago) by jyh
File length: 21996 byte(s)
Diff to previous 2376
Added #quit directive, and interactive_flag to reduce output in
non-interactive sessions.


Revision 2376 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jul 31 14:35:45 1998 UTC (22 years, 10 months ago) by jyh
File length: 21707 byte(s)
Diff to previous 2336
Added TPTP theory, and Ensemble library.  Fixed sequent displays.
BUG: rewrites fail on sequents.


Revision 2336 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jul 21 22:47:13 1998 UTC (22 years, 11 months ago) by jyh
File length: 21392 byte(s)
Diff to previous 2307
Added NL toploop so that we can compile NL native code.


Revision 2307 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jul 6 17:55:31 1998 UTC (22 years, 11 months ago) by nogin
File length: 18360 byte(s)
Diff to previous 2283
Removed $Log messages from all NL files.


Revision 2283 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jul 2 18:38:08 1998 UTC (22 years, 11 months ago) by jyh
File length: 20529 byte(s)
Diff to previous 2280
Refiner modules now raise RefineError exceptions directly.
Modules in this revision have two versions: one that raises
verbose exceptions, and another that uses a generic exception.


Revision 2280 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jul 1 04:38:04 1998 UTC (22 years, 11 months ago) by nogin
File length: 20783 byte(s)
Diff to previous 2244
Moved Refiner exceptions into a separate module RefineErrors


Revision 2244 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jun 15 22:33:52 1998 UTC (23 years ago) by jyh
File length: 20665 byte(s)
Diff to previous 2224
Added CZF.


Revision 2224 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 12 13:47:49 1998 UTC (23 years ago) by jyh
File length: 19642 byte(s)
Diff to previous 2209
D tactic works, added itt_bool.


Revision 2209 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jun 1 13:57:13 1998 UTC (23 years ago) by jyh
File length: 18715 byte(s)
Diff to previous 2201
Proving twice one is two.


Revision 2201 - (view) (download) (annotate) - [select for diffs]
Modified Fri May 29 14:53:34 1998 UTC (23 years ago) by jyh
File length: 17940 byte(s)
Diff to previous 2190
Better Makefiles.


Revision 2190 - (view) (download) (annotate) - [select for diffs]
Modified Thu May 28 13:48:44 1998 UTC (23 years ago) by jyh
File length: 15280 byte(s)
Diff to previous 2171
Updated the editor to use new Refiner structure.
ITT needs dform names.


Revision 2171 - (view) (download) (annotate) - [select for diffs]
Modified Thu May 7 16:03:13 1998 UTC (23 years, 1 month ago) by jyh
File length: 15184 byte(s)
Diff to previous 2166
Adding interactive proofs.


Revision 2166 - (view) (download) (annotate) - [select for diffs]
Modified Mon May 4 23:46:19 1998 UTC (23 years, 1 month ago) by jyh
File length: 15033 byte(s)
Diff to previous 2156
Most display forms now work.


Revision 2156 - (view) (download) (annotate) - [select for diffs]
Modified Tue Apr 28 18:31:05 1998 UTC (23 years, 1 month ago) by jyh
File length: 14929 byte(s)
Diff to previous 2153
ls() works, adding display.


Revision 2153 - (view) (download) (annotate) - [select for diffs]
Modified Fri Apr 24 19:39:13 1998 UTC (23 years, 2 months ago) by jyh
File length: 10962 byte(s)
Diff to previous 2152
Updated debugging.


Revision 2152 - (view) (download) (annotate) - [select for diffs]
Modified Fri Apr 24 02:44:07 1998 UTC (23 years, 2 months ago) by jyh
File length: 10840 byte(s)
Diff to previous 2151
Added more extensive debugging capabilities.


Revision 2151 - (view) (download) (annotate) - [select for diffs]
Modified Thu Apr 23 20:04:52 1998 UTC (23 years, 2 months ago) by jyh
File length: 10624 byte(s)
Diff to previous 2138
Initial rebuilt editor.


Revision 2138 - (view) (download) (annotate) - [select for diffs]
Modified Fri Apr 17 02:25:32 1998 UTC (23 years, 2 months ago) by jyh
File length: 10007 byte(s)
Diff to previous 2137
Implementing shell.


Revision 2137 - (view) (download) (annotate) - [select for diffs]
Modified Fri Apr 17 01:31:36 1998 UTC (23 years, 2 months ago) by jyh
File length: 10829 byte(s)
Diff to previous 2047
Editor is almost constructed.


Revision 2047 - (view) (download) (annotate) - [select for diffs]
Added Wed Aug 6 16:18:55 1997 UTC (23 years, 10 months ago) by jyh
File length: 12563 byte(s)
This is an ocaml version with subtyping, type inference,
d and eqcd tactics.  It is a basic system, but not debugged.


This form allows you to request diffs between any two revisions of this file. For each of the two "sides" of the diff, enter a numeric revision.

  Diffs between and
  Type of Diff should be a

  ViewVC Help
Powered by ViewVC 1.1.26