/[mojave]/metaprl/theories/czf/Makefile
ViewVC logotype

Log of /metaprl/theories/czf/Makefile

Parent Directory Parent Directory | Revision Log Revision Log


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

Revision 3566 - (view) (download) (annotate) - [select for diffs]
Modified Tue Apr 9 05:56:39 2002 UTC (19 years, 2 months ago) by xiny
File length: 1153 byte(s)
Diff to previous 3548
Updated to reflect new file names.


Revision 3548 - (view) (download) (annotate) - [select for diffs]
Modified Sun Mar 24 08:29:36 2002 UTC (19 years, 3 months ago) by xiny
File length: 1077 byte(s)
Diff to previous 3517
Updated to reflect new file names.


Revision 3517 - (view) (download) (annotate) - [select for diffs]
Modified Mon Feb 25 21:18:49 2002 UTC (19 years, 3 months ago) by xiny
File length: 1025 byte(s)
Diff to previous 3404
Added czf_itt_equiv to MPFILES


Revision 3404 - (view) (download) (annotate) - [select for diffs]
Modified Sun Sep 23 07:25:28 2001 UTC (19 years, 9 months ago) by xiny
File length: 1009 byte(s)
Diff to previous 3380
1. Minor changes in czf_itt_group;
2. Define subgroup and abelian group;
3. Define cyclic subgroup and cyclic group. However, there are
   problems with the proofs in czf_itt_cyclic_subgroup.


Revision 3380 - (view) (download) (annotate) - [select for diffs]
Modified Fri Sep 14 07:05:10 2001 UTC (19 years, 9 months ago) by xiny
File length: 920 byte(s)
Diff to previous 3292
Definitions for set difference & Boolean set


Revision 3292 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jun 24 10:25:49 2001 UTC (19 years, 11 months ago) by nogin
File length: 871 byte(s)
Diff to previous 3158
*** IMPORTANT: before doing "cvs update" see warning below ***

This commit implements a global resource that brings together resource management
that used to be done by each resource in its own way.

- A much simplier object (Mp_resource.resource_info) is now needed to create a new resource.
Additionally, many resource helper modules, such as term_match_table now provide functions
that create a resource_info for you.

- Funtions get_tactic_arg, get_int_tactic_arg, etc were replaced by a single function
get_resource_arg (note: functions for basci types, such as get_with_arg, get_sel_args, etc
were _not_ affected)

- Resource declaration statement now declares and resource creation statement now creates
a function get_<name>_resource. This function ca be passed as a second argument
to get_resource_arg to retrieve the current value of a particular resource.

- Resource annotation functions are now separate from the resource declaration/creation
mechanism. Resource annotation on a rule are now passed to a function named
process_<name>_resource_annotation. This function must have the appropriate
Mp_resource.annotation_processor type for the resource. This function can be declared
and implemented in _any_ module, not just the module that declares and creates the
<name> resource.

- Currenlty MetaPRL leaves it to Ocaml to keep track of these functions.
Consequently the module that defines the process_<name>_resource_annotation function
must be open'ed (not included!) by modules that use <name> annotations.

-----

Unfinished business in this commit:
- Remainder of TODO 1.12 and 1.13

- Some proofs were broken by this commit. It appears that they were broken for
a "good" reason, but still need to be fixed.

- I need to make sure things now always have the right precedences (all things being equal,
the later an item is added to resource, the earlier precedence it should have).

- Consider adding refiner sentinels and display forms to global resource as well.
Currently each of them still does its own way of resource management (although the way
display forms are managed was changed by this commit - need to make sure the precedences
are right).

- Distributed refinement: I am afraid that the current resource code
will either work correctly only if all processes in the distributed group have
the same global resource, or it will attempt to pass around all the resource data.
Obviously, neither of these choices is a good one.

*** WARNING ***

This commit changes the tactic_arg type and also makes minor changes in
the FilterCache.info type. Because of that old .prlb and .cmoz files
*will no longer work*. Old .prla files will work, but will produce lots
of (harmless) Filter_summary.dest_term warning.

Before doing "cvs update" do the following:
1) export all your unsaved proofs into .prla files.
2) rm -f theories/*/*.prlb
3) run "make clean"


Revision 3158 - (view) (download) (annotate) - [select for diffs]
Modified Sat Feb 24 12:25:11 2001 UTC (20 years, 3 months ago) by nogin
File length: 857 byte(s)
Diff to previous 3057
TODO: Better matching in dT
make: added an .mlz file to the appropriate variable.


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: 827 byte(s)
Diff to previous 3052
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 3052 - (view) (download) (annotate) - [select for diffs]
Modified Wed Aug 30 00:56:48 2000 UTC (20 years, 9 months ago) by jyh
File length: 757 byte(s)
Diff to previous 2901
Two changes.
   1. expand () now does sloppy expansion, so that proofs
      can be replayed even if the goal of a proof has changed.
      This also means that proof copy/paste should work.

   2. I fixed up CZF.  This is a pretty cool set theory, where
      we get the usual ZF axioms (except excluded middle).  The
      normal things like numbers can be coded in the usual
      way, except we get decidability of number equality and
      other constructive ideas.  Reals can be coded with
      Dedekind cuts according to Aczel.  This theory is the
      basic set theory with just the axioms.  Before going on,
      it is probably a good idea to stratify the sets with
      levels, so we can formalize the notion of classes.


Revision 2901 - (view) (download) (annotate) - [select for diffs]
Modified Tue Feb 22 00:40:43 2000 UTC (21 years, 4 months ago) by nogin
File length: 664 byte(s)
Diff to previous 2775
Added profiling comtrol to some tests

Added explicit include of the mk/preface to some Makefiles


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: 635 byte(s)
Diff to previous 2763
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 2763 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jun 29 03:40:34 1999 UTC (21 years, 11 months ago) by nogin
File length: 632 byte(s)
Diff to previous 2743
Removed -I $(ROOT)/lib from the INCLUDES.
It was unnecessary since mk/rules adds -I $(ROOT)/lib to ocaml{c,opt} calls anyway.


Revision 2743 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 23 04:50:29 1999 UTC (22 years ago) by jyh
File length: 647 byte(s)
Diff to previous 2711
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 2711 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jun 14 03:32:18 1999 UTC (22 years ago) by nogin
File length: 636 byte(s)
Diff to previous 2582
cvf_theory is not an MLZFILE and should not be mentioned in Makefile


Revision 2582 - (view) (download) (annotate) - [select for diffs]
Modified Tue Feb 2 01:54:59 1999 UTC (22 years, 4 months ago) by nogin
File length: 677 byte(s)
Diff to previous 2497
- Now all user configuration options are in mk/config file
- The old mk/config file (the one with all the make rules)
  is now called mk/rules, the new mk/config is _not_ on CVS
- When mk/config.init is newer than mk/config (e.g. mk/config
  does not exist), mk/config.init is appended to mk/config
- Toplevel Makefile checks if mk/config definies everything
  it should define and prints an error message if not

- Fixed a bug in refiner/refsig/refine_error.h that prevented
  SIMPLE refiner from being built

- I was not able to completely check if everything works because
  of the bug introduced by the previous check-in


Revision 2497 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 13 01:52:18 1998 UTC (22 years, 8 months ago) by nogin
File length: 678 byte(s)
Diff to previous 2367
Renaming it in Makefiles:
NLLIB -> MPLIB, NLFILES -> MPFILES, NL2FILES -> MP2FILES, etc.


Revision 2367 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jul 27 02:02:43 1998 UTC (22 years, 10 months ago) by nogin
File length: 678 byte(s)
Diff to previous 2333
Use $(RM) instead of del or rm -f


Revision 2333 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jul 17 15:39:32 1998 UTC (22 years, 11 months ago) by jyh
File length: 679 byte(s)
Diff to previous 2325
CZF is complete, although we may wish to add pairing and inf.


Revision 2325 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jul 14 15:44:03 1998 UTC (22 years, 11 months ago) by jyh
File length: 531 byte(s)
Diff to previous 2320
Intermediate version with auto tactic.


Revision 2320 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jul 9 21:08:59 1998 UTC (22 years, 11 months ago) by jyh
File length: 602 byte(s)
Diff to previous 2314
Upgraded czf.


Revision 2314 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jul 8 15:42:11 1998 UTC (22 years, 11 months ago) by jyh
File length: 588 byte(s)
Diff to previous 2309
Pushed higherC into the refiner for efficiency.


Revision 2309 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jul 6 21:39:34 1998 UTC (22 years, 11 months ago) by jyh
File length: 555 byte(s)
Diff to previous 2283
Working czf_itt_set.


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: 540 byte(s)
Diff to previous 2272
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 2272 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jun 23 22:12:44 1998 UTC (23 years ago) by jyh
File length: 547 byte(s)
Diff to previous 2251
Improved rewriter speed with conversion tree and flist.


Revision 2251 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jun 16 16:26:27 1998 UTC (23 years ago) by jyh
File length: 434 byte(s)
Diff to previous 2245
Added itt_test.


Revision 2245 - (view) (download) (annotate) - [select for diffs]
Added Mon Jun 15 22:41:33 1998 UTC (23 years ago) by jyh
File length: 421 byte(s)
Added Makefile.


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