Please find, for review, the debconf templates and packages descriptions for the proofgeneral source package.
This review will last from Friday, October 26, 2007 to Monday, November 05, 2007.
Please send reviews as unified diffs (diff -u) against the original
files. Comments about your proposed changes will be appreciated.
Your review should be sent as an answer to this mail.
When appropriate, I will send intermediate requests for review, with
"[RFRn]" (n>=2) as a subject tag.
When we will reach a consensus, I send a "Last Chance For
Comments" mail with "[LCFC]" as a subject tag.
Finally, the reviewed templates will be sent to the package maintainer
as a bug report, and a mail will be sent to this list with "[BTS]" as
a subject tag.
Rationale:
--- ../proofgeneral.old/debian/proofgeneral.templates 2007-10-22 08:02:33.596937437 +0200
+++ debian/proofgeneral.templates 2007-10-25 07:38:48.149570244 +0200
@@ -1,14 +1,14 @@
Template: proofgeneral/autoload
Type: boolean
Default: true
-_Description: Should Proof General be auto-loaded by default at your site?
- If you want to auto-load Proof General at your site, you should accept
- here.
+_Description: Should Proof General be auto-loaded by default?
+ Please choose this option if you want to auto-load Proof General
+ on this machine.
I don't really see the value added by "at your site". Moreover, I
think this brings Emacs jargon ("site") which does not really bring
much information.
Use the now well standardized "Please choose this option...." wording.
.
- If you accept, Proof General is loaded globally, i.e. all people in
- your site can use Proof General at any time in their Emacs or XEmacs
- without special settings in their "~/.emacs".
+ If you do so, it will be loaded globally and all local users will
+ be able to use it with Emacs or XEmacs,
+ without special settings in their personal configuration file.
Re-word and slightly dejargonize...as well as avoid the latin "i.e."
.
- If you refuse, people who desire to use it will have to either edit
- "~/.emacs" or start a Proof General session explicitly with the
- proofgeneral command.
+ If you don't choose this option, users will need to activate it
+ from their personal settings for Emacs or XEmacs, or start it
+ explicitly with the 'proofgeneral' command.
s/people/users and similar rewording.
--- ../proofgeneral.old/debian/control 2007-10-22 08:02:33.596937437 +0200
+++ debian/control 2007-10-25 07:42:57.137235252 +0200
@@ -10,62 +10,60 @@
Depends: debconf | debconf-2.0, emacs22 | emacsen
Suggests: x-symbol
Recommends: proofgeneral-misc | proofgeneral-coq
-Description: A generic interface for proof assistants
+Description: generic interface for proof assistants - common package
Proof General is a generic interface for proof assistants,
currently based on the customizable text editor Emacs.
- It works with either XEmacs or GNU Emacs. Proof General
- has been developed at the LFCS in the University of Edinburgh.
+ It works with either XEmacs or GNU Emacs.
+ .
+ Proof General has been developed at the LFCS in the University of
+ Edinburgh.
Avoid leading article in synopsis
Use a "generic description - specific description" layout for synopsis
Split in paragraphs. I however think that mentioning the origin of the
software in the description is pointless (even if it will make one of
our reviewers happy).
I think that all this description is missing what a "proof assistant"
is. From the context in the following packages, one can guess this is
about mathematics.
Package: proofgeneral-coq
Architecture: all
Depends: proofgeneral
Recommends: coq
-Description: ProofGeneral support for coq
- This package provides the Proof General support for the Coq
- theorem prover which is available as another package. Though
- it is not required to just edit Coq files.
- .
+Description: generic interface for proof assistants - coq support
"generic - specific"
Proof General is a generic interface for proof assistants,
currently based on the customizable text editor Emacs.
- It works with either XEmacs or GNU Emacs. Proof General
- has been developed at the LFCS in the University of Edinburgh.
+ It works with either XEmacs or GNU Emacs.
+ .
+ This package provides the Proof General support for the Coq
+ theorem prover which is available as another package. The
+ package is however not required to just edit Coq files.
Standardize the specific paragraph.
...similar changes to all other packages.
Template: proofgeneral/autoload Type: boolean Default: true _Description: Should Proof General be auto-loaded by default? Please choose this option if you want to auto-load Proof General on this machine. . If you do so, it will be loaded globally and all local users will be able to use it with Emacs or XEmacs, without special settings in their personal configuration file. . If you don't choose this option, users will need to activate it from their personal settings for Emacs or XEmacs, or start it explicitly with the 'proofgeneral' command.
--- proofgeneral.old/debian/proofgeneral.templates 2007-10-22 08:02:33.596937437 +0200 +++ proofgeneral/debian/proofgeneral.templates 2007-10-26 18:05:46.471570139 +0200 @@ -1,14 +1,14 @@ Template: proofgeneral/autoload Type: boolean Default: true -_Description: Should Proof General be auto-loaded by default at your site? - If you want to auto-load Proof General at your site, you should accept - here. +_Description: Should Proof General be auto-loaded by default? + Please choose this option if you want to auto-load Proof General + on this machine. . - If you accept, Proof General is loaded globally, i.e. all people in - your site can use Proof General at any time in their Emacs or XEmacs - without special settings in their "~/.emacs". + If you do so, it will be loaded globally and all local users will + be able to use it with Emacs or XEmacs, + without special settings in their personal configuration file. . - If you refuse, people who desire to use it will have to either edit - "~/.emacs" or start a Proof General session explicitly with the - proofgeneral command. + If you don't choose this option, users will need to activate it + from their personal settings for Emacs or XEmacs, or start it + explicitly with the 'proofgeneral' command. --- proofgeneral.old/debian/control 2007-10-22 08:02:33.596937437 +0200 +++ proofgeneral/debian/control 2007-10-25 07:42:57.137235252 +0200 @@ -10,62 +10,60 @@ Depends: debconf | debconf-2.0, emacs22 | emacsen Suggests: x-symbol Recommends: proofgeneral-misc | proofgeneral-coq -Description: A generic interface for proof assistants +Description: generic interface for proof assistants - common package Proof General is a generic interface for proof assistants, currently based on the customizable text editor Emacs. - It works with either XEmacs or GNU Emacs. Proof General - has been developed at the LFCS in the University of Edinburgh. + It works with either XEmacs or GNU Emacs. + . + Proof General has been developed at the LFCS in the University of + Edinburgh. Package: proofgeneral-coq Architecture: all Depends: proofgeneral Recommends: coq -Description: ProofGeneral support for coq - This package provides the Proof General support for the Coq - theorem prover which is available as another package. Though - it is not required to just edit Coq files. - . +Description: generic interface for proof assistants - coq support Proof General is a generic interface for proof assistants, currently based on the customizable text editor Emacs. - It works with either XEmacs or GNU Emacs. Proof General - has been developed at the LFCS in the University of Edinburgh. + It works with either XEmacs or GNU Emacs. + . + This package provides the Proof General support for the Coq + theorem prover which is available as another package. The + package is however not required to just edit Coq files. Package: proofgeneral-minlog Architecture: all Depends: proofgeneral, mzscheme (>= 300) | guile Recommends: minlog -Description: ProofGeneral support for Minlog - This package provides the Proof General support for the Minlog - theorem prover which is available as another package. Though - it is not required to just edit Minlog files. - . +Description: generic interface for proof assistants - Minlog support Proof General is a generic interface for proof assistants, currently based on the customizable text editor Emacs. - It works with either XEmacs or GNU Emacs. Proof General - has been developed at the LFCS in the University of Edinburgh. + It works with either XEmacs or GNU Emacs. + . + This package provides the Proof General support for the Minlog + theorem prover which is available as another package. The + package is however not required to just edit Minlog files. Package: proofgeneral-misc Architecture: all Depends: proofgeneral -Description: ProofGeneral support for different theorem provers - This package provides the Proof General support for several - theorem provers which are not available as Debian packages yet. - This includes: ACL2, HOL98, Isabelle, Isar, LClam, LEGO, - Phox, Plastic, Twelf - . +Description: generic interface for proof assistants - theorem provers support Proof General is a generic interface for proof assistants, currently based on the customizable text editor Emacs. - It works with either XEmacs or GNU Emacs. Proof General - has been developed at the LFCS in the University of Edinburgh. + It works with either XEmacs or GNU Emacs. + . + This package provides the Proof General support for several + theorem provers which are not available as packages yet. + This includes: ACL2, HOL98, Isabelle, Isar, LClam, LEGO, + Phox, Plastic, Twelf. Package: proofgeneral-doc Architecture: all -Description: Documentation for ProofGeneral in html format - This package provides the html documentation for Proof General. - It was created from the same sources as the info documentation - which is included in the proofgeneral package. - . +Description: generic interface for proof assistants - documentation Proof General is a generic interface for proof assistants, currently based on the customizable text editor Emacs. - It works with either XEmacs or GNU Emacs. Proof General - has been developed at the LFCS in the University of Edinburgh. + It works with either XEmacs or GNU Emacs. + . + This package provides the HTML documentation for Proof General. + It was created from the same sources as the info documentation + which is included in the proofgeneral package.
Source: proofgeneral Section: editors Priority: optional Maintainer: Stefan Schimanski <schimmi@debian.org> Build-Depends: debhelper (>= 4.1.16), po-debconf Standards-Version: 3.7.2 Package: proofgeneral Architecture: all Depends: debconf | debconf-2.0, emacs22 | emacsen Suggests: x-symbol Recommends: proofgeneral-misc | proofgeneral-coq Description: generic interface for proof assistants - common package Proof General is a generic interface for proof assistants, currently based on the customizable text editor Emacs. It works with either XEmacs or GNU Emacs. . Proof General has been developed at the LFCS in the University of Edinburgh. Package: proofgeneral-coq Architecture: all Depends: proofgeneral Recommends: coq Description: generic interface for proof assistants - coq support Proof General is a generic interface for proof assistants, currently based on the customizable text editor Emacs. It works with either XEmacs or GNU Emacs. . This package provides the Proof General support for the Coq theorem prover which is available as another package. The package is however not required to just edit Coq files. Package: proofgeneral-minlog Architecture: all Depends: proofgeneral, mzscheme (>= 300) | guile Recommends: minlog Description: generic interface for proof assistants - Minlog support Proof General is a generic interface for proof assistants, currently based on the customizable text editor Emacs. It works with either XEmacs or GNU Emacs. . This package provides the Proof General support for the Minlog theorem prover which is available as another package. The package is however not required to just edit Minlog files. Package: proofgeneral-misc Architecture: all Depends: proofgeneral Description: generic interface for proof assistants - theorem provers support Proof General is a generic interface for proof assistants, currently based on the customizable text editor Emacs. It works with either XEmacs or GNU Emacs. . This package provides the Proof General support for several theorem provers which are not available as packages yet. This includes: ACL2, HOL98, Isabelle, Isar, LClam, LEGO, Phox, Plastic, Twelf. Package: proofgeneral-doc Architecture: all Description: generic interface for proof assistants - documentation Proof General is a generic interface for proof assistants, currently based on the customizable text editor Emacs. It works with either XEmacs or GNU Emacs. . This package provides the HTML documentation for Proof General. It was created from the same sources as the info documentation which is included in the proofgeneral package.
Attachment:
signature.asc
Description: Digital signature