rpms/zenon/F-8 zenon-format.5, NONE, 1.1 zenon.1, NONE, 1.1 import.log, 1.1, 1.2 zenon.spec, 1.2, 1.3

Fri Jul 25 19:56:39 UTC 2008

Author: dwheeler

Update of /cvs/pkgs/rpms/zenon/F-8
In directory cvs-int.fedora.redhat.com:/tmp/cvs-serv15357/F-8

Modified Files:
	import.log zenon.spec 
Added Files:
	zenon-format.5 zenon.1 
Log Message:

* Fri Jun 27 2008 David A. Wheeler - 0.5.0-3
- Add documentation for Zenon and its built-in format as man pages
  (man pages used so Debian, etc., will use them too)
- Fix release number so it increases everywhere

--- NEW FILE zenon-format.5 ---
.TH ZENON-FORMAT "5" "2008-07" "David A. Wheeler" "User Commands"
.SH NAME
zenon-format \- Automated theorem prover for first-order classical logic format
.SH DESCRIPTION
.\" Add any additional description here
.PP
Zenon can use several input formats, including its own "Zenon" format.
This document describes this "Zenon" format.
.PP
In the Zenon format,
"#" and ";" introduce comments that continue to the end of the line.
Identifiers begin with A-Z, a-z, or underscore; they may continue with
0 or more of the characters A-Z, a-z, 0-9, underscore, and apostrophe.
Strings are enclosed inside double-quote characters; they may not contain
the double-quote character, control characters, or characters beyond 126.
Whitespace is a token separator, but is otherwise ignored.
Its syntax is as follows:
.RS
file:
  | EOF
  | phrase file

phrase:
  | DEF "(" IDENT ident_list ")" expr
  | HYP int_opt hyp_name expr
  | GOAL expr
  | SIG IDENT "(" string_list ")" STRING
  | INDSET IDENT "(" ident_list ")"

expr:
  | IDENT
  | "(" IDENT expr_list ")"
  | "(" NOT expr ")"
  | "(" AND expr expr_list ")"
  | "(" OR expr expr_list ")"
  | "(" IMPLY expr expr_list ")"
  | "(" RIMPLY expr expr_list ")"
  | "(" EQUIV expr expr_list ")"
  | "(" TRUE ")"
  | TRUE
  | "(" FALSE ")"
  | FALSE
  | "(" ALL mlambda ")"
  | "(" EX mlambda ")"
  | mlambda
  | "(" TAU lambda ")"
  | "(" "=" expr expr ")"
  | "(" MATCH expr case_list ")"
  | "(" LET id_expr_list_expr ")"

expr_list:
  | expr expr_list
  | /* empty */

lambda:
  | "(" "(" IDENT STRING ")" expr ")"
  | "(" "(" IDENT ")" expr ")"

mlambda:
  | "(" "(" ident_list STRING ")" expr ")"
  | "(" "(" ident_list ")" expr ")"

ident_list:
  | /* empty */
  | IDENT ident_list

int_opt:
  | /* empty */
  | INT

hyp_name:
  | /* empty */
  | STRING

string_list:
  | /* empty */
  | STRING string_list

case_list:
  | /* empty */
  | "(" IDENT ident_list ")" expr case_list

id_expr_list_expr:
  | expr
  | IDENT expr id_expr_list_expr

.RE
.PP
With the following token definitions:
.RS
 DEF "$def"
 GOAL "$goal"
 HYP "$hyp"
 INDSET "$indset"
 INDPROP "$indprop"
 LET "$let"
 MATCH "$match"
 SIG "$sig"
 NOT "-."
 AND "/\\"
 OR "\\/"
 IMPLY "=>"
 RIMPLY "<="
 EQUIV "<=>"
 TRUE "T."
 FALSE "F."
 ALL "A."
 EX "E."
 TAU "t."
.RE

.SH "SEE ALSO"
.PP
zenon(1)

.SH AUTHOR
.PP
This man page was written by David A. Wheeler.
.SH COPYRIGHT
Zenon is released under the revised BSD license.
This man page is released under both the revised BSD and MIT licenses
(your choice).



--- NEW FILE zenon.1 ---
.TH ZENON "1" "2008-07" "David A. Wheeler" "User Commands"
.SH NAME
zenon \- Automated theorem prover for first-order classical logic
.SH SYNOPSIS
.B zenon
[\fIOPTIONS\fR] \fIFILE\fR
.SH DESCRIPTION
.\" Add any additional description here
.PP
Zenon is an automated theorem prover for first order classical logic
with equality, based on the tableau method.
Zenon can read input files in TPTP, Coq, Focal, and its own Zenon format.
Zenon can directly generate Coq proofs (proof scripts or proof terms),
which can be reinserted into Coq specifications.
Zenon can also be extended.
.SH OPTIONS
.PP
.\" Mandatory arguments to long options are mandatory for short options too.
If file is "-", it will read input from stdin.
.TP 10
\fB\-context\fR
provide context for checking the proof independently
.TP 10
\fB\-d\fR
debug mode
.TP 10
\fB\-errmsg\fR \fI<message>\fR
prefix warnings and errors with \fI<message>\fR
.TP 10
\fB\-help\fR, \fB\--help\fR
print this option list and exit
.TP 10
\fB\-I\fR \fI<dir>\fR
add \fI<dir>\fR to the include path (for TPTP input format)
.TP 10
\fB\-icoq\fR
read input file in Coq format
.TP 10
\fB\-ifocal\fR
read input file in Focal format
.TP 10
\fB\-itptp\fR
read input file in TPTP format
.TP 10
\fB\-iz\fR
read input file in Zenon format (default)
.TP 10
\fB\-loadpath\fR
path to Zenon's coq libraries (default /usr/share/zenon)
.TP 10
\fB\-max\fR \fI<s>[kMGT]/<i>[kMGT]/<t>[smhd]\fR
set size, step, and time limits
.TP 10
\fB\-max-size\fR \fI<s>[kMGT]\fR
limit heap size to <s> kilo/mega/giga/tera word (default 100M)
.TP 10
\fB\-max-step\fR \fI<i>[kMGT]\fR
limit number of steps to <s> kilo/mega/giga/tera (default 10k)
.TP 10
\fB\-max-time\fR \fI<t>[smhd]\fR
limit CPU time to <t> second/minute/hour/day (default 5m)
.TP 10
\fB\-ocoq\fR
print the proof in Coq script format
.TP 10
\fB\-ocoqterm\fR
print the proof in Coq term format
.TP 10
\fB\-oh\fR
<n>             print the proof in high-level format up to depth <n>
.TP 10
\fB\-ol\fR
print the proof in low-level format
.TP 10
\fB\-olx\fR
print the proof in raw low-level format
.TP 10
\fB\-om\fR
print the proof in middle-level format
.TP 10
\fB\-onone\fR
do not print the proof (default)
.TP 10
\fB\-opt0\fR
do not optimise the proof
.TP 10
\fB\-opt1\fR
do peephole optimisation of the proof (default)
.TP 10
\fB\-p0\fR
turn off progress bar and progress messages
.TP 10
\fB\-p1\fR
display progress bar (default)
.TP 10
\fB\-p2\fR
display progress messages
.TP 10
\fB\-q\fR
(quiet) suppress proof-found/no-proof/begin-proof/end-proof
.TP 10
\fB\-rename\fR
prefix all input symbols to avoid clashes
.TP 10
\fB\-rnd\fR \fI<seed>\fR
randomize proof search
.TP 10
\fB\-stats\fR
print statistics
.TP 10
\fB\-short\fR
output a less detailed proof
.TP 10
\fB\-v\fR
print version string and exit
.TP 10
\fB\-versions\fR
print CVS version strings and exit
.TP 10
\fB\-w\fR
suppress warnings
.TP 10
\fB\-where\fR
print the location of the zenon library and exit
.TP 10
\fB\-wout\fR \fI<file>\fR
output errors and warnings to \fI<file>\fR instead of stderr
.TP 10
\fB\-x\fR \fI<ext>\fR
activate extension \fI<ext>\fR

.SH EXAMPLE
.PP
The command:
.RS
  \fCzenon -itptp -ocoq /usr/share/zenon*/examples/tptp-COM003+2.p\fP
.RE
will take the input file "tptp-COM003+2.p" in TPTP format (-itptp),
search for a proof, and produce any proof output in Coq format (-ocoq).
tptp-COM003+2.p is a TPTP representation of the halting problem.
Zenon can prove this, and will print out:
.RS
\fC(* PROOF-FOUND *)\fP
.br
\fC(* BEGIN-PROOF *)\fP
.br
... details of proof in Coq format
.br
\fC(* END-PROOF *)\fP
.RE

.\" TO DO: .SH EXIT STATUS
.SH "SEE ALSO"
.PP
zenon-format(5)

.SH AUTHOR
.PP
This man page was written by David A. Wheeler.
.SH COPYRIGHT
Zenon is released under the revised BSD license.
This man page is released under both the revised BSD and MIT licenses
(your choice).



Index: import.log
===================================================================
RCS file: /cvs/pkgs/rpms/zenon/F-8/import.log,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -r1.1 -r1.2
--- import.log	21 Jul 2008 16:44:04 -0000	1.1
+++ import.log	25 Jul 2008 19:56:09 -0000	1.2
@@ -1 +1,2 @@
 zenon-0_5_0-2_fc9:F-8:zenon-0.5.0-2.fc9.src.rpm:1216658626
+zenon-0_5_0-3_fc9:F-8:zenon-0.5.0-3.fc9.src.rpm:1217015751


Index: zenon.spec
===================================================================
RCS file: /cvs/pkgs/rpms/zenon/F-8/zenon.spec,v
retrieving revision 1.2
retrieving revision 1.3
diff -u -r1.2 -r1.3
--- zenon.spec	21 Jul 2008 17:38:33 -0000	1.2
+++ zenon.spec	25 Jul 2008 19:56:09 -0000	1.3
@@ -1,6 +1,6 @@
 Name:		zenon
 Version:	0.5.0
-Release:	2.1%{?dist}
+Release:	3%{?dist}
 Summary:	Automated theorem prover for first-order classical logic
 Group:		Applications/Engineering
 License:	BSD
@@ -8,6 +8,9 @@
 Source0:	http://focal.inria.fr/zenon/zenon-0.5.0.tar.gz
 Source1:	zenon-tptp-COM003+2.p
 Source2:	zenon-tptp-ReadMe
+# Basic documentation (man pages). Submitted upstream 2008-07-25:
+Source3:	zenon.1
+Source4:	zenon-format.5
 Patch0 :	zenon.bytecode.patch
 BuildRoot:	%{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n)
 BuildRequires:	ocaml >= 3.08
@@ -42,6 +45,10 @@
 cp -p %{SOURCE2} tptp-ReadMe
 chmod g-w tptp*
 
+cp -p %{SOURCE3} %{SOURCE4} .
+gzip zenon.1
+gzip zenon-format.5
+
 # Work around Makefile errors (fails if no ocamlopt, uses _bytecode_ otherwise)
 %if %opt
   make %{?_smp_mflags} zenon.opt
@@ -58,41 +65,24 @@
   %define __os_install_post /usr/lib/rpm/brp-compress %{nil}
 %endif
 
-# Create stub documentation; upstream has NOTHING.
-cat > zenon-doc.txt <<ENDSTUB
-Zenon is an automated theorem prover for first order classical logic
-with equality, based on the tableau method.
-
-Usage Example:
-  zenon -itptp -ocoq %{_docdir}/%{name}-%{version}/examples/tptp-COM003+2.p
-
-  This will take the input file "tptp-COM003+2.p" in TPTP format (-itptp),
-  search for a proof, and produce any proof output in Coq format (-ocoq).
-  tptp-COM003+2.p is a TPTP representation of the halting problem.
-  Zenon can prove this, and will print out:
-  (* PROOF-FOUND *)
-  (* BEGIN-PROOF *)
-  ... details of proof in Coq format
-  (* END-PROOF *)
-
-You can learn more about the Thousands of Problems for Theorem Provers
-(TPTP) Problem Library and its input format from http://www.tptp.org.
-
-
-ENDSTUB
-./zenon --help >> zenon-doc.txt 2>&1
 
 %install
 rm -rf %{buildroot}
 install -d %{buildroot}/%{_bindir}/
 install -d %{buildroot}/%{_libdir}/
-install -d %{buildroot}/%{_defaultdocdir}/%{name}-%{version}/examples/
 
 make install DESTDIR=%{buildroot}
+
+install -d %{buildroot}/%{_defaultdocdir}/%{name}-%{version}/examples/
+cp -p LICENSE %{buildroot}/%{_defaultdocdir}/%{name}-%{version}/
 cp -p tptp-COM003+2.p tptp-ReadMe \
  %{buildroot}/%{_defaultdocdir}/%{name}-%{version}/examples/
 
-cp -p LICENSE zenon-doc.txt %{buildroot}/%{_defaultdocdir}/%{name}-%{version}/
+install -d %{buildroot}%{_mandir}/man1/
+install -d %{buildroot}%{_mandir}/man5/
+cp -p zenon.1.gz %{buildroot}%{_mandir}/man1/
+cp -p zenon-format.5.gz %{buildroot}%{_mandir}/man5/
+
 
 
 %check
@@ -119,11 +109,18 @@
 %{_defaultdocdir}/%{name}-%{version}/
 %{_bindir}/*
 %{_datadir}/%{name}/
+%{_mandir}/man1/*
+%{_mandir}/man5/*
 
 
 %changelog
+* Fri Jun 27 2008 David A. Wheeler - 0.5.0-3
+- Add documentation for Zenon and its built-in format as man pages
+  (man pages used so Debian, etc., will use them too)
+- Fix release number so it increases everywhere
+
 * Fri Jun 27 2008 David A. Wheeler - 0.5.0-2.1
-- macro fc8 failed.
+- macro fc8 failed, minor rebuild for Fedora 8
 
 * Fri Jun 27 2008 David A. Wheeler - 0.5.0-2
 - Moved examples to an "examples" subdirectory in /usr/share/doc/NAME-VERSION


