/[mojave]/metaprl/doc/latex/theories
ViewVC logotype

Log of /metaprl/doc/latex/theories

View Directory Listing Directory Listing


Sticky Revision:

Revision 3591 - Directory Listing
Modified Sun Apr 28 19:51:58 2002 UTC (19 years, 1 month ago) by nogin
- 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 3587 - Directory Listing
Modified Sat Apr 27 02:43:27 2002 UTC (19 years, 1 month ago) by emre
Adding file to specify which modules to print documentation for.
(And adding .cvsignore to ignore generated files.)


Revision 3584 - Directory Listing
Modified Thu Apr 25 15:28:40 2002 UTC (19 years, 2 months ago) by nogin
- 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 3410 - Directory Listing
Modified Tue Sep 25 16:52:43 2001 UTC (19 years, 9 months ago) by nogin
- 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 3329 - Directory Listing
Modified Fri Jul 13 21:34:19 2001 UTC (19 years, 11 months ago) by nogin
I've removed old Itt_int* theories and switched all the ITT to Yegor's
new theories.


Revision 3298 - Directory Listing
Modified Mon Jun 25 01:34:52 2001 UTC (20 years ago) by kopylov
- 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 3232 - Directory Listing
Modified Thu May 17 22:06:20 2001 UTC (20 years, 1 month ago) by nogin
I joined Itt_hide and Itt_squash into a single theory - Itt_squash that deals
with both the meta-level squash operator (Base_trivial!squash{}) and the type
theory squash operator (Itt_squash!squash{'A}). This makes sense because
these two operators are almost exectly the same in nature except for oe
being a meta-level operator and another - an object-level one.

This commit also renames Itt_hide!hide into Itt_squash!squash. This means
that we now have two operators named "squash", however this should not cause
any confusion since all part of the system (including the parser and display
form mechanism) take into account the number of arguments.

Warning: This commit probably broke lots of proofs. I plan to fix that
after I have a chance to rewrite the squash theory a little better (for
now I just copied the one from Itt_hide). Hopefully, I should have it
done within a week.


Revision 3231 - Directory Listing
Modified Tue May 15 07:10:57 2001 UTC (20 years, 1 month ago) by nogin
Use Mozilla when available.


Revision 3140 - Directory Listing
Modified Mon Feb 5 00:38:18 2001 UTC (20 years, 4 months ago) by kopylov
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 3115 - Directory Listing
Modified Fri Jan 26 21:15:20 2001 UTC (20 years, 4 months ago) by kopylov
I have added a new theory Itt_struct2 with some derived advanced versions of
substitution rules and the cut rule.
In particular, I have proved the let (cutEq) rule (that is the cut rule for the membership).

Itt_struct2 redefines the substT tactic to use stronger substitution rules.
There are also new tactics: letT, assetEqT and assertHideT.

Itt_theory does not include Itt_struct2. If you whant to use these rules, you need to include
Itt_struct2 explicitly.


Revision 3088 - Directory Listing
Modified Fri Nov 10 20:23:06 2000 UTC (20 years, 7 months ago) by nogin
Small fixes.


Revision 3071 - Directory Listing
Modified Sat Sep 23 03:47:08 2000 UTC (20 years, 9 months ago) by kopylov
I split the Itt_set theory into Itt_hide and Itt_set.
Note that now the term hide declared in Itt_hide theory, not in Itt_set.
Let me know if you have problems with this.

Now hide(A) is a full-fledged type.
We can use it not only for hiding hypothesis,
but also anywhere in a sequent.

By definition hide(A) is empty if A is empty and has only one
element "it" otherwise.


Revision 3068 - Directory Listing
Modified Thu Sep 21 21:18:56 2000 UTC (20 years, 9 months ago) by nogin
- Added ~ and sqeq to parser. For now, they produce Perv!"rewrite" terms,
but once the new rewriting mechanisms are implemented, we'll be able to
change them to produce "sqeq" opname in "local" theory. I also changed all
ITT conditional rewrites from Perv!"rewrite" to ~.

- "make clean" now cleans all the new stuff Jason added to doc/{ps,latex}


Revision 3067 - Directory Listing
Modified Wed Sep 20 22:30:03 2000 UTC (20 years, 9 months ago) by kopylov
1)	Added a new theory (itt_disect) about dependent intersection.

2)	Fixed rules intersectionElimination and intersectionSubtype in itt_isect

3)	Added a correct version of  intersectionMemberFormation

4)	Fixed some comments

5)	Added a new bug (4.10) in BUGS


Revision 3066 - Directory Listing
Modified Tue Sep 19 22:18:30 2000 UTC (20 years, 9 months ago) by nogin
- Ocamldep now treats "derive" in the same way as "include" and "open"
(instead of just ignoring it) which recovered some missing dependencies
in the FOL theory.

- Better TeX dependencies, including "make tex" now noticing when
a theory changes.

- Section hack - now Index and Bibliography are created as normal section
(without two separate "Index" headings as it used to be).


Revision 3065 - Directory Listing
Modified Tue Sep 19 16:46:39 2000 UTC (20 years, 9 months ago) by jyh
Fall back to CM fonts in the all-theories.tex file.
This should fix problem with missing LB (Lucida Bright) fonts.
My copy of acrobat 4.0 has no trouble reading the result of pdflatex,
let me know if there are still problems.


Revision 3064 - Directory Listing
Modified Tue Sep 19 06:36:31 2000 UTC (20 years, 9 months ago) by nogin
Documentation Makefiles hacking:
- Added "texbyte and texopt" in edimor/ml to force using byetcode/native code
MetaPRL for generating TeX files. "make tex" would use opt if available
and bytecode otherwise.

- More dependencies to make sure the files are being regenerated as necessary.


Revision 3062 - Directory Listing
Modified Tue Sep 19 03:03:23 2000 UTC (20 years, 9 months ago) by jyh
Sorry, the problem with the last commit was just because of the
theories/base/base_theory.mlz, which used @begin[tex] instead
of @begin[doc].  Everything should compile now.

Once it compiles, try using make in the doc/latex/theories
directory.  It should generate the file all-theories.pdf, which
is docs for all the modules, including tactics, rules, rewrites,
etc.  There is an index that you can use to jump to the documentation
for any particular tactic, etc.


Revision 3057 - Directory Listing
Added Sun Sep 10 18:26:37 2000 UTC (20 years, 9 months ago) by jyh
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.


  ViewVC Help
Powered by ViewVC 1.1.26