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