Re: Proposed new feature: Provers

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

 



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

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Index of Archives]     [Fedora Announce]     [Fedora Kernel]     [Fedora Testing]     [Fedora Formulas]     [Fedora PHP Devel]     [Kernel Development]     [Fedora Legacy]     [Fedora Maintainers]     [Fedora Desktop]     [PAM]     [Red Hat Development]     [Gimp]     [Yosemite News]
  Powered by Linux