Proposed new feature: Provers

[Vasile Gaburici]

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