On Sun, Feb 22, 2009 at 09:57:04AM +0100, Petr Pudlak wrote:
> * Package name : eprover
> Description : The Equational Theorem Prover E
That is not a description, that is just the name spelled out. A better
description would be "equational theorem prover".
> E is an automated equational theorem prover. That means it is a program that
> you can stuff a mathematical specification (in first-order logic with equality)
> and a hypothesis into,
So far so good...
> and which will then run forever, using up all of your
> machines resources. Very occasionally it will find a proof for the hypothesis
> and tell you so ;-).
If I read this, I think: "What kind of crap software is this that suffers from
infinite loops and only works for only a handful of equations? Why is it in
Debian if there are other theorem provers that are apparently better?"
> Release 1.0 is the culmination of a long development phase. Important changes
> vs. version 0.999 include the fixing of some bugs in definitional
> clausification for large problems and general cleanup.
That information belongs in the upstream NEWS or Changes file, not in a package
description.
> (Copied from the original documentation.)
Ok. But this is not suited for a package description. Please create a better
description that is more serious, and explains what this prover can and cannot
do. Have a look at packages from similar software, like prover9, if you need
inspiration.
--
Met vriendelijke groet / with kind regards,
Guus Sliepen <guus@debian.org>
Attachment:
signature.asc
Description: Digital signature