"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@xxxxxxxxxxxxxxxxx> 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@xxxxxxxxxx > https://www.redhat.com/mailman/listinfo/fedora-devel-list > > -- fedora-devel-list mailing list fedora-devel-list@xxxxxxxxxx https://www.redhat.com/mailman/listinfo/fedora-devel-list
