Sorry, I misunderstood your 1st email; I thought the list contained
stuff already packaged...
As for volunteering for HOL: if I package it, the 10% or so of
functionality I've ever used will work, the rest - who knows. The
problem with packaging tools normally used by a niche audience is that
unless you're part of the niche experts, you don't have much clue if
the package is well done or not, even more so when it comes to
handling bug reports.
I care a lot more about seeing TeXLive 2008 rather than HOL in F10,
but even that is probably not going to happen. On a strictly volunteer
basis I cannot afford the time to package complex software I seldom
use...
On Fri, Aug 8, 2008 at 6:49 AM, David A. Wheeler <dwheeler(a)dwheeler.com> wrote:
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(a)redhat.com
https://www.redhat.com/mailman/listinfo/fedora-devel-list