FAQ Search Today's Posts Mark Forums Read
» Video Reviews

» Linux Archive

Linux-archive is a website aiming to archive linux email lists and to make them easily accessible for linux users/developers.


» Sponsor

» Partners

» Sponsor

Go Back   Linux Archive > Redhat > Fedora Development

 
 
LinkBack Thread Tools
 
Old 08-07-2008, 09:18 PM
"David A. Wheeler"
 
Default Proposed new featu Provers

I've developed info on a new feature of Fedora 10, aka "Provers":
https://fedoraproject.org/wiki/Features/Provers
Basically, I and others have packaged some key
provers / solvers / formal methods tools.

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

You can find their descriptions and URLs here:
http://www.dwheeler.com/essays/high-assurance-floss.html

--- David A. Wheeler

--
fedora-devel-list mailing list
fedora-devel-list@redhat.com
https://www.redhat.com/mailman/listinfo/fedora-devel-list
 
Old 08-07-2008, 09:27 PM
Rahul Sundaram
 
Default Proposed new featu Provers

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@redhat.com
https://www.redhat.com/mailman/listinfo/fedora-devel-list
 
Old 08-07-2008, 09:39 PM
Jarod Wilson
 
Default Proposed new featu Provers

On Thursday 07 August 2008 17:18:21 David A. Wheeler wrote:
> I've developed info on a new feature of Fedora 10, aka "Provers":
> https://fedoraproject.org/wiki/Features/Provers
> Basically, I and others have packaged some key
> provers / solvers / formal methods tools.

As I understand it, this is primarily just a collection of new packages being
added to Fedora, no? If so, and if you ask me, this really doesn't meet the
criteria for a Feature. Its just new packages that are all targeted at a
specific area of use.

--
Jarod Wilson
jwilson@redhat.com

--
fedora-devel-list mailing list
fedora-devel-list@redhat.com
https://www.redhat.com/mailman/listinfo/fedora-devel-list
 
Old 08-07-2008, 09:41 PM
"Vasile Gaburici"
 
Default Proposed new featu Provers

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

--
fedora-devel-list mailing list
fedora-devel-list@redhat.com
https://www.redhat.com/mailman/listinfo/fedora-devel-list
 
Old 08-07-2008, 10:05 PM
"Vasile Gaburici"
 
Default Proposed new featu Provers

Also, you may want to take a look at this Fedora repository:
http://math.ifi.uzh.ch/fedora/
It contains gap (gap-system.org) and twelf (twelf.plparty.org) amongst
other things.

On Fri, Aug 8, 2008 at 12:41 AM, Vasile Gaburici <vgaburici@gmail.com> wrote:
> "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@fedoraproject.org> 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@redhat.com
>> https://www.redhat.com/mailman/listinfo/fedora-devel-list
>>
>>
>

--
fedora-devel-list mailing list
fedora-devel-list@redhat.com
https://www.redhat.com/mailman/listinfo/fedora-devel-list
 
Old 08-08-2008, 03:49 AM
"David A. Wheeler"
 
Default Proposed new featu Provers

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@redhat.com
https://www.redhat.com/mailman/listinfo/fedora-devel-list
 
Old 08-08-2008, 05:28 AM
"Vasile Gaburici"
 
Default Proposed new featu Provers

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

--
fedora-devel-list mailing list
fedora-devel-list@redhat.com
https://www.redhat.com/mailman/listinfo/fedora-devel-list
 
Old 08-08-2008, 06:41 AM
"Miles Sabin"
 
Default Proposed new featu Provers

On Thu, Aug 7, 2008 at 10:18 PM, David A. Wheeler <dwheeler@dwheeler.com> wrote:
> Can anyone help us package some additional programs?
> Some potential ones include:

Would it be appropriate to add Agda2 to this list?

http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php

I have a rough and ready .spec file, but taking it further has been
stalled waiting on the Haskell packaging guidelines and cabal-rpm to
be finalized.

Cheers,


Miles

--
fedora-devel-list mailing list
fedora-devel-list@redhat.com
https://www.redhat.com/mailman/listinfo/fedora-devel-list
 
Old 08-08-2008, 10:45 AM
"Richard W.M. Jones"
 
Default Proposed new featu Provers

On Thu, Aug 07, 2008 at 05:18:21PM -0400, David A. Wheeler wrote:
> https://fedoraproject.org/wiki/Features/Provers

You might want to consider adding CIL to the list. It's already in
Fedora (as 'ocaml-cil'), I use it quite a bit, but the package needs a
little love & I would appreciate a co-maintainer with some time to fix
some of the packaging bugs and keep up with upstream versions.

For anyone wondering about CIL, it's a brilliant C parser and static
analysis tool, quite simple to use, which supports gcc extensions and
can be used to analyze the Linux kernel and other significant C
programs. I wrote a quick intro here with some pretty pictures:

http://et.redhat.com/~rjones/cil-analysis-of-libvirt/

Rich.

--
Richard Jones, Emerging Technologies, Red Hat http://et.redhat.com/~rjones
virt-df lists disk usage of guests without needing to install any
software inside the virtual machine. Supports Linux and Windows.
http://et.redhat.com/~rjones/virt-df/

--
fedora-devel-list mailing list
fedora-devel-list@redhat.com
https://www.redhat.com/mailman/listinfo/fedora-devel-list
 
Old 08-08-2008, 01:06 PM
Andrew Overholt
 
Default Proposed new featu Provers

Hi,

* David A. Wheeler <dwheeler@dwheeler.com> [2008-08-07 17:19]:
> I've developed info on a new feature of Fedora 10, aka "Provers":
> https://fedoraproject.org/wiki/Features/Provers

sat4j is currently in Fedora if that's of interest to you.

Andrew

--
fedora-devel-list mailing list
fedora-devel-list@redhat.com
https://www.redhat.com/mailman/listinfo/fedora-devel-list
 

Thread Tools




All times are GMT. The time now is 08:47 AM.

VBulletin, Copyright ©2000 - 2014, Jelsoft Enterprises Ltd.
Content Relevant URLs by vBSEO ©2007, Crawlability, Inc.
Copyright 2007 - 2008, www.linux-archive.org