Proposed new feature: Provers

[David A. Wheeler]

Vasile Gaburici:
>"Provers" is a bit narrow. Maybe use "theorem proving tools" so we can
>include Coq

By "provers" I certainly include Coq; see the web page.
Coq is an interactive theorem prover, while Zenon is an
automated theorem prover.  Both provers, methinks.

>which Fedora already ships, in the category?
>... Also add zenon to the
>category, since Fedora already includes it as well.

Actually, the original Fedora 9 release did NOT include Coq or Zenon.
Coq and Zenon are two of the packages we _specifically_ worked to add.
We've also made them available to Fedora 9 (and where sensible 8 too).

> Btw, make sure that HOL works; the authors love to complain that all
> Linux distros ship it broken!

We don't have HOL packaged yet.  Volunteering?

We've certainly had "fun" getting things to work together.
Why, for example, generated an old Zenon format, so they
didn't work together.  But this is the reason for packaging, to
make them work together.  If it's broken, please let the packager
know so it can get fixed...!

--- David A. Wheeler