/[mojave]/metaprl/theories/tactic/nuprl_font.ml
ViewVC logotype

Log of /metaprl/theories/tactic/nuprl_font.ml

Parent Directory Parent Directory | Revision Log Revision Log


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

Revision 3591 - (view) (download) (annotate) - [select for diffs]
Modified Sun Apr 28 19:51:58 2002 UTC (19 years, 1 month ago) by nogin
File length: 42602 byte(s)
Diff to previous 3532
- Added an option to be have "THEORIES=all" in mk/config
(instead of THEORIES="long list of theories").
I will change all my nightly scripts to use THEORIES=all.

- Added mc to the default list of TEXTHEORIES. Added a file all-bodies.tex
that would automatically contain \inputs corresponding to TEXTHEORIES.
(Before this change we had to update all-theories.tex by hands whenever TEXTHEORIES
was changed).

- Minor fixes in some display forms.

- Removed theories/caml that never had anything useful.

- Removed a few files from theories/ocaml_doc that seemed to be there by accident
(Jason, can you confirm?).


Revision 3532 - (view) (download) (annotate) - [select for diffs]
Modified Sun Mar 10 23:29:54 2002 UTC (19 years, 3 months ago) by nogin
File length: 42449 byte(s)
Diff to previous 3410
I am committing David Bustos' changes to the cons build system for Metaprl.

See David's message "cons for MetaPRL" in the newsgroup for more information -
news://news.metaprl.org:119/20020310131332.A13595@wink.caltech.edu


Revision 3410 - (view) (download) (annotate) - [select for diffs]
Modified Tue Sep 25 16:52:43 2001 UTC (19 years, 8 months ago) by nogin
File length: 42477 byte(s)
Diff to previous 3396
- Merged the Ocaml 3.02 changes

- Now http server is compiled in by default, but is only started if
the "-http true" argument is passed or MP_HTTP environment variable
is set to "true".

- A few other minor changes.


Revision 3396 - (view) (download) (annotate) - [select for diffs]
Modified Fri Sep 21 14:22:55 2001 UTC (19 years, 9 months ago) by nogin
File length: 42449 byte(s)
Diff to previous 3299
- Added proper escaping of <, > and & in html Rformat output
- Goal and Subgoal window updates are now done in separate threads
- Updated some homepages URLs in mp-people.html


Revision 3299 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jun 26 14:08:42 2001 UTC (19 years, 11 months ago) by nogin
File length: 42688 byte(s)
Diff to previous 3298
sub/sup should assume math mode.


Revision 3298 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jun 25 01:34:52 2001 UTC (20 years ago) by kopylov
File length: 42692 byte(s)
Diff to previous 3254
- All rules in record theories are prooved (except some simple arith facts).

- Now progressT checks whether the assumptions are changed (not only the goal).

- Add a new operator tsquash{A}={Top|A}


Revision 3254 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jun 7 19:14:04 2001 UTC (20 years ago) by nogin
File length: 42113 byte(s)
Diff to previous 3236
- For symbolic keywords, use tt instead of bf
- Use tt for non-math < and > to make sure that are displayed properly.


Revision 3236 - (view) (download) (annotate) - [select for diffs]
Modified Wed May 23 15:42:53 2001 UTC (20 years, 1 month ago) by nogin
File length: 41580 byte(s)
Diff to previous 3235
- Proved all the theorems in itt_squash.
- Still need to figure out the right way to do squash_resource and
the relevant tactics.


Revision 3235 - (view) (download) (annotate) - [select for diffs]
Modified Sun May 20 23:04:08 2001 UTC (20 years, 1 month ago) by nogin
File length: 41514 byte(s)
Diff to previous 3223
Display form fixes.

- TeX: all object-level terms (theorem statements, etc) are now typeset
in math mode.

- Tex: variable names are now parsed to detect indeces. In particular,
  'a1 will now be printed as a_{1} and 'a1_2 will be printed as a_{1,2}.

- Tex: `|' symbol in display forms is now always handled correctly.

- Numerous small fixes.


Revision 3223 - (view) (download) (annotate) - [select for diffs]
Modified Tue May 8 23:59:11 2001 UTC (20 years, 1 month ago) by nogin
File length: 41483 byte(s)
Diff to previous 3140
Finally, I am able to commit what I was getting to
in all these commits over the last several days.

I changed the parser to index declared opnames by its "shape" -
last string of opname + parameter types + subterm arities
instead of just the last string (as it used to be). This means that
the parser now checks whether the usage of an opname corresponds
to its declaration. This allowed me to detect numerous typos in
display forms and even some rules and rewrites and, hopefully,
will prevent people from making such typos in the future.

This is only the first pass of the implementation. I still need to:
- make sure none of my fixes broke any display forms that used to work
  because of typos cancelling each other
- update the documentation
- implement checking of shapes on the opnames specified using the
  Module!name notation (currently no checking is done on such opnames)


Revision 3140 - (view) (download) (annotate) - [select for diffs]
Modified Mon Feb 5 00:38:18 2001 UTC (20 years, 4 months ago) by kopylov
File length: 41286 byte(s)
Diff to previous 3058
For now 'a~'b produces Itt_squiggle!sqeq{'a;'b} rather then Perv!rewrite.

I documented the Itt_squiggle theory (see all-theories.pdf).


Revision 3058 - (view) (download) (annotate) - [select for diffs]
Modified Sun Sep 10 20:41:19 2000 UTC (20 years, 9 months ago) by jyh
File length: 41288 byte(s)
Diff to previous 3050
Last commit failed partway through...


Revision 3050 - (view) (download) (annotate) - [select for diffs]
Modified Sun Aug 20 01:40:18 2000 UTC (20 years, 10 months ago) by nogin
File length: 40403 byte(s)
Diff to previous 2822
- I added my personal TODO file that contains a list of things
that I am considering doing with/in/about/around MetaPRL

- I fixed the display form modes in ITT!!!
1) I added the except_mode[...] display form option. It is opposite
to the mode[...] option. The main idea was to be able to say
except_mode[src]
2) I made sure all the display forms in ITT (and below it, except for
Ocaml) are annotated with proper mode and except_mode options.
3) I added (in one of the previous commits) the  set_dfmode
command to MetaPRL toploop. Now  set_dfmode "src"  can be used
to produce terms in a form suitable for cutting and pasting into
.ml files and command line tactic arguments.
4) I updated the documentation accordingly.


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: 38670 byte(s)
Diff to previous 2812
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 2812 - (view) (download) (annotate) - [select for diffs]
Modified Tue Sep 7 00:44:30 1999 UTC (21 years, 9 months ago) by jyh
File length: 38698 byte(s)
Diff to previous 2809
Finally fixed the tutorial so that we have a derivation of
classical first-order logic.  The HTML docs are not yet up-to-date.


Revision 2809 - (view) (download) (annotate) - [select for diffs]
Modified Tue Aug 31 17:31:53 1999 UTC (21 years, 9 months ago) by jyh
File length: 38699 byte(s)
Diff to previous 2808
Display changes to get Java to work a little better.


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: 41491 byte(s)
Diff to previous 2743
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 2743 - (view) (download) (annotate) - [select for diffs]
Added Wed Jun 23 04:50:29 1999 UTC (22 years ago) by jyh
File length: 26510 byte(s)
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


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