Proposed new feature: Provers

[Vasile Gaburici]

Also, you may want to take a look at this Fedora repository:
http://math.ifi.uzh.ch/fedora/
It contains gap (gap-system.org) and twelf (twelf.plparty.org) amongst
other things.

On Fri, Aug 8, 2008 at 12:41 AM, Vasile Gaburici <vgaburici at gmail.com> wrote:
> "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
>>
>>
>