4:18 p.m.
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
4:27 p.m.
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
4:41 p.m.
"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(a)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(a)redhat.com
https://www.redhat.com/mailman/listinfo/fedora-devel-list
5:05 p.m.
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(a)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(a)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(a)redhat.com
> https://www.redhat.com/mailman/listinfo/fedora-devel-list
>
>
4:39 p.m.
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(a)redhat.com
8:30 a.m.
Jarod Wilson wrote:
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.
And what criteria are those? I don't think this is the first feature
that has been mostly a packaging affair. Last I checked our definition
of feature was "something worth mentioning in the release notes."
--CJD
9 a.m.
On Fri, Aug 08, 2008 at 09:30:28AM -0400, Casey Dahlin wrote:
>
And what criteria are those? I don't think this is the first feature
that has been mostly a packaging affair. Last I checked our definition
of feature was "something worth mentioning in the release notes."
I agree. Here the issue is merely communicating something new and nice.
Alan is willing to do the associated paperwork so this is certainly a
feature.
--
Pat
9:20 a.m.
On Fri, 2008-08-08 at 16:00 +0200, Patrice Dumas wrote:
On Fri, Aug 08, 2008 at 09:30:28AM -0400, Casey Dahlin wrote:
>>
> And what criteria are those? I don't think this is the first feature
> that has been mostly a packaging affair. Last I checked our definition
> of feature was "something worth mentioning in the release notes."
I agree. Here the issue is merely communicating something new and nice.
Alan is willing to do the associated paperwork so this is certainly a
feature.
Haskell support is a feature; is there a reason why this shouldn't be as
well?
--
Paul W. Frields
gpg fingerprint: 3DA6 A0AC 6D58 FEC4 0233 5906 ACDB C937 BD11 3717
http://paul.frields.org/ - - http://pfrields.fedorapeople.org/
irc.freenode.net: stickster @ #fedora-docs, #fedora-devel, #fredlug
11:14 a.m.
Paul W. Frields wrote:
On Fri, 2008-08-08 at 16:00 +0200, Patrice Dumas wrote:
> On Fri, Aug 08, 2008 at 09:30:28AM -0400, Casey Dahlin wrote:
>>>
>> And what criteria are those? I don't think this is the first feature
>> that has been mostly a packaging affair. Last I checked our definition
>> of feature was "something worth mentioning in the release notes."
> I agree. Here the issue is merely communicating something new and nice.
> Alan is willing to do the associated paperwork so this is certainly a
> feature.
Haskell support is a feature; is there a reason why this shouldn't be as
well?
I think it depends on how its written up. For instance, this past FESCo
meeting, there was a Feature Proposal: python-nss -- python bindings to
libnss.
Really that's just a package, not a feature. However, if it was written
as "Take steps to make FIPS 140 verification possible" and this was one
of the steps taken, it would be a better Feature proposal. (Being able
to say we've converted foo, bar, and baz important programs or X number
of programs to python-nss would make it better yet).
So similarly, just saying Fedora has a collection of provers isn't a
Feature. But saying, in Fedora 10 we've made an effort to include foo,
bar, baz important provers for Target Audience so they can find all the
tools they need to do X Type of Work. Similarly, "We've done work so
that foo and bar can import and export the same file format", or other
work to show how we're making the user experience better would make a
stronger case for a feature.
-Toshio
1:15 p.m.
On Friday 08 August 2008 09:30:28 Casey Dahlin wrote:
Jarod Wilson wrote:
> 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.
And what criteria are those? I don't think this is the first feature
that has been mostly a packaging affair. Last I checked our definition
of feature was "something worth mentioning in the release notes."
http://fedoraproject.org/wiki/Features/Policy/Is_this_a_feature
http://fedoraproject.org/wiki/Features/Policy/Definitions
I suppose perhaps this falls under "noteworthy enough to call out in the
release notes", depending on who you ask. I'm still not sold yet.
On Friday 08 August 2008 mumble, Toshio Kuratomi wrote:
[...] just saying Fedora has a collection of provers isn't a
Feature. But saying, in Fedora 10 we've made an effort to include foo,
bar, baz important provers for Target Audience so they can find all the
tools they need to do X Type of Work. Similarly, "We've done work so
that foo and bar can import and export the same file format", or other
work to show how we're making the user experience better would make a
stronger case for a feature.
Like Toshio suggests here, sell me on the idea. Right now, all I see is a
group of new packages that are similar in nature.
--
Jarod Wilson
jwilson(a)redhat.com
3:20 p.m.
Perhaps creating a new group in comps.xml would be appropriate? I'll
let you judge if that in itself would qualify as new feature, but it
will be noticeable to people that care - academics mostly. But RHEL
sell ok in academia, so it should be worth doing :)
On Fri, Aug 8, 2008 at 9:15 PM, Jarod Wilson <jwilson(a)redhat.com> wrote:
On Friday 08 August 2008 09:30:28 Casey Dahlin wrote:
> Jarod Wilson wrote:
> > 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.
>
> And what criteria are those? I don't think this is the first feature
> that has been mostly a packaging affair. Last I checked our definition
> of feature was "something worth mentioning in the release notes."
http://fedoraproject.org/wiki/Features/Policy/Is_this_a_feature
http://fedoraproject.org/wiki/Features/Policy/Definitions
I suppose perhaps this falls under "noteworthy enough to call out in the
release notes", depending on who you ask. I'm still not sold yet.
On Friday 08 August 2008 mumble, Toshio Kuratomi wrote:
> [...] just saying Fedora has a collection of provers isn't a
> Feature. But saying, in Fedora 10 we've made an effort to include foo,
> bar, baz important provers for Target Audience so they can find all the
> tools they need to do X Type of Work. Similarly, "We've done work so
> that foo and bar can import and export the same file format", or other
> work to show how we're making the user experience better would make a
> stronger case for a feature.
Like Toshio suggests here, sell me on the idea. Right now, all I see is a
group of new packages that are similar in nature.
--
Jarod Wilson
jwilson(a)redhat.com
--
fedora-devel-list mailing list
fedora-devel-list(a)redhat.com
https://www.redhat.com/mailman/listinfo/fedora-devel-list
1:41 a.m.
On Thu, Aug 7, 2008 at 10:18 PM, David A. Wheeler <dwheeler(a)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
5:45 a.m.
On Thu, Aug 07, 2008 at 05:18:21PM -0400, David A. Wheeler wrote:
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/
8:06 a.m.
Hi,
* David A. Wheeler <dwheeler(a)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
5766
days inactive
5767
days old
14 comments
11 participants
participants (11)
-
Andrew Overholt -
Casey Dahlin -
David A. Wheeler -
Jarod Wilson -
Miles Sabin -
Patrice Dumas -
Paul W. Frields -
Rahul Sundaram -
Richard W.M. Jones -
Toshio Kuratomi -
Vasile Gaburici