ViewVC logotype

Log of /metaprl/refiner/reflib/Files

Parent Directory Parent Directory | Revision Log Revision Log

Links to HEAD: (view) (download) (annotate)
Sticky Revision:

Revision 2920 - (view) (download) (annotate) - [select for diffs]
Modified Mon Mar 13 23:02:21 2000 UTC (21 years, 4 months ago) by steph
File length: 415 byte(s)
Diff to previous 2919
 Enter Log.  Lines beginning with `CVS:' are removed automatically

 Committing in .

 Modified Files:

Revision 2919 - (view) (download) (annotate) - [select for diffs]
Modified Mon Mar 13 22:17:11 2000 UTC (21 years, 4 months ago) by steph
File length: 436 byte(s)
Diff to previous 2887
 Enter Log.  Lines beginning with `CVS:' are removed automatically

 Committing in .

 Modified Files:
 	jall.ml jall.mli Files
 Added Files:
 	jtunify.mli jtunify.ml

Revision 2887 - (view) (download) (annotate) - [select for diffs]
Modified Thu Feb 17 23:04:30 2000 UTC (21 years, 5 months ago) by nogin
File length: 406 byte(s)
Diff to previous 2880
Some .mlz files were not marked as such in Makefiles - fixed

Revision 2880 - (view) (download) (annotate) - [select for diffs]
Modified Wed Feb 2 18:19:32 2000 UTC (21 years, 6 months ago) by steph
File length: 416 byte(s)
Diff to previous 2743
*** empty log message ***

Revision 2743 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 23 04:50:29 1999 UTC (22 years, 1 month ago) by jyh
File length: 384 byte(s)
Diff to previous 2732
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.

   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

   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).


Revision 2732 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 18 04:51:42 1999 UTC (22 years, 1 month ago) by nogin
File length: 362 byte(s)
Diff to previous 2602
Added support for ASCII-based term IO. I tested the code a lot and it seems working,
but it is not integrated into the system yet. And simple_name_* functions need to be
improved if we want ASCII theory files to be at least sligtly readable.

Revision 2602 - (view) (download) (annotate) - [select for diffs]
Modified Fri Feb 26 00:37:49 1999 UTC (22 years, 5 months ago) by nogin
File length: 336 byte(s)
Diff to previous 2601
Made TermHeader, TermHash and TermNorm a part of the term module

Revision 2601 - (view) (download) (annotate) - [select for diffs]
Modified Thu Feb 25 17:59:51 1999 UTC (22 years, 5 months ago) by nogin
File length: 395 byte(s)
Diff to previous 2594
1) Functorized the Term_copy[2]_weak/Term_hash/Termm_header/etc modules
correctly, now it should be easy make the Term_hash module
a part of the refiner

2) Created a new Term_io module that provides Refiner_std <-> Refiner
convertion based on the term_copy2_weak, these functions are now used
instead of the old Term_copy functions

3) Removed old Term_copy - related modules

Revision 2594 - (view) (download) (annotate) - [select for diffs]
Modified Tue Feb 16 16:53:19 1999 UTC (22 years, 5 months ago) by nogin
File length: 426 byte(s)
Diff to previous 2580
Added the new weak term_copy files into the build (they are being built,
but not being used yet).

Revision 2580 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jan 31 21:42:08 1999 UTC (22 years, 6 months ago) by jyh
File length: 332 byte(s)
Diff to previous 2576
Added "simp" and "verb" rules to Makefiles.  There are no *.mlp and *.mlip
files in the refiner any longer.  Instead, the C-preprocessor is run at
compile time.

By default, the verbose refiner is generated.  To get the others, use
make simp, or make opt_simp.

Revision 2576 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jan 28 03:57:07 1999 UTC (22 years, 6 months ago) by nogin
File length: 340 byte(s)
Diff to previous 2520
Added some simple code to match two hypothesis lists.
It does not always do the right thing, but would probably
succeed in many cases

Revision 2520 - (view) (download) (annotate) - [select for diffs]
Modified Sun Nov 29 23:28:38 1998 UTC (22 years, 8 months ago) by nogin
File length: 326 byte(s)
Diff to previous 2494
Added the bi-directional Term_copy module
written by Yegon Bryukhov <yegor@lpcs.math.msu.ru>

This version is undebugged and is very slow:
it seems to be quadratic and also it becomes much slower
after each invocation.

Revision 2494 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 13 01:14:08 1998 UTC (22 years, 9 months ago) by jyh
File length: 257 byte(s)
Diff to previous 2443
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 2443 - (view) (download) (annotate) - [select for diffs]
Modified Mon Aug 24 13:43:48 1998 UTC (22 years, 11 months ago) by jyh
File length: 257 byte(s)
Diff to previous 2356
Slightly better Ensemble scheduling.
Native-code compiler has trouble marshaling functions--
its probably a problem with the marshaler.

Added Nl_num, a ML-only implementation of bignums.
This is slower than the C version used by OCaml, but
we can marshal the Nl_nums.  Most of the files changed
are just replacements of Num.* with Nl_num.*.

Revision 2356 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jul 24 21:11:12 1998 UTC (23 years ago) by nogin
File length: 254 byte(s)
Diff to previous 2291
Functorized the Simple_print module over the Refiner module

Revision 2291 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jul 3 22:06:15 1998 UTC (23 years, 1 month ago) by jyh
File length: 235 byte(s)
Diff to previous 2284
IO terms are now in term_std format.

Revision 2284 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jul 2 22:25:40 1998 UTC (23 years, 1 month ago) by jyh
File length: 235 byte(s)
Diff to previous 2256
Created term_copy module to copy and normalize terms.

Revision 2256 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 17 13:18:33 1998 UTC (23 years, 1 month ago) by jyh
File length: 223 byte(s)
Diff to previous 2222
Added ml_term.

Revision 2222 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jun 9 20:53:04 1998 UTC (23 years, 1 month ago) by jyh
File length: 213 byte(s)
Diff to previous 2195
Propagated refinement changes.
New tacticals module.

Revision 2195 - (view) (download) (annotate) - [select for diffs]
Added Fri May 29 00:42:17 1998 UTC (23 years, 2 months ago) by jyh
File length: 229 byte(s)
File listings.

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