Proposed new feature: Provers

[Vasile Gaburici]

"Provers" is a bit narrow. Maybe use "theorem proving tools" so we can
include Coq, which Fedora already ships, in the category? For the
uninformed: Coq is only a proof assistant. Also add zenon to the
category, since Fedora already includes it as well.

Btw, make sure that HOL works; the authors love to complain that all
Linux distros ship it broken!
<from their web page>
Warning: Pre-packaged versions of Isabelle, Proof General, and Poly/ML
floating through the Net as deb, rpm, port etc. are often outdated and
rarely work as advertized. Even XEmacs is better compiled manually
these days -- the packages provided for SuSE, Ubuntu, and Debian are
mostly broken.
</duh>

On Fri, Aug 8, 2008 at 12:27 AM, Rahul Sundaram
<sundaram at fedoraproject.org> wrote:
> David A. Wheeler wrote:
>>
>> Can anyone help us package some additional programs?
>> Some potential ones include:
>> * ACL2 (I have a start at this, it's written in Common Lisp)
>> * haRVey-FOL (depends on E and SPASS)
>> * BLAST, at http://mtc.epfl.ch/software-tools/blast/ (don't use the
>> obsolete version at Berkeley)
>> * HOL 4
>> * Isabelle
>> * HOL Lite
>> * Gandalf
>> * NuSMV
>> * DiVinE
>> * KeY
>>
>
> It would be quite useful if you add more information, classify them as easy,
> medium, hard similar to the OLPC packages wishlist, the language being used
> etc. I saw them on the packager wishlist and went through a couple which
> seemed a large amount of pain to package.  I am wondering if all of these
> are in the similar category.
>
> Rahul
>
> --
> fedora-devel-list mailing list
> fedora-devel-list at redhat.com
> https://www.redhat.com/mailman/listinfo/fedora-devel-list
>
>