DevHeads.net

Proposal for new package group: Development:Formal Methods Tools

I would like to edit comps.xml to add a new package group for the tools
that have already been packaged by the Formal Methods SIG.

I propose that the group be located under the "Development" category.

Id: formal-methods-tools
Name: Formal Methods Tools
Description: These tools for the development of hardware and software are based on Formal proof methods.

The default for the group itself will be false (will not be installed by
default). Find below a list of package names to be included in the group
with the proposed level (D for default, O for optional). Given that the
scope of application of these tools is very diverse, it made sense to
me to make most of the packages optional;

O alt-ergo
O alt-ergo-gui
O coq
O coq-coqide
O coq-doc
O coq-emacs
O coq-emacs-el
O cryptominisat
O cryptominisat-devel
O csisat
O cudd
O cvc3
O cvc3-devel
O cvc3-doc
O cvc3-emacs
O cvc3-emacs-el
O cvc3-java
O cvc3-xemacs
O cvc3-xemacs-el
O E
O emacs-common-proofgeneral
O emacs-proofgeneral
O emacs-proofgeneral-el
O flocq
O flocq-source
D frama-c
O gappa
O gappalib-coq
O glueminisat
D minisat2
O picosat
D prover9
O prover9-apps
O prover9-devel
O prover9-doc
O pvs-sbcl
O sat4j
O stp
O stp-devel
O tex-zfuzz
O why
O why-all
O why-coq
O why-gwhy
O why-jessie
O why-pvs-support
O why3
O why3-emacs
O zenon

More information on these packages can be found on the wiki here:

<a href="https://fedoraproject.org/wiki/Formal_methods_tool_suite" title="https://fedoraproject.org/wiki/Formal_methods_tool_suite">https://fedoraproject.org/wiki/Formal_methods_tool_suite</a>
<a href="https://fedoraproject.org/wiki/FormalMethods" title="https://fedoraproject.org/wiki/FormalMethods">https://fedoraproject.org/wiki/FormalMethods</a>

Regards, John

Comments

Re: Proposal for new package group: Development:Formal Methods T

By Christopher Meng at 08/24/2013 - 03:17

在 2013-8-18 AM3:31,"John C. Peterson" < ... at eskimo dot com>写道:
I just want to know if Group tag is needed or not, I never add Group tag in
any specs of mine.

Proposal for new package group: Development:Formal Methods Tools

By John C. Peterson at 08/25/2013 - 16:14

On Sat, Aug 24, 2013 at 03:17:39PM +0800, Christopher Meng wrote:
I was referring to the groups defined in comps.xml which is used by the
installer during during the software selection phase of installation.

The legal values of group tags that go in rpm spec files are documented
in /usr/share/doc/rpm-4.x.x.x/GROUPS

I guess it's apropos to call the larger picture here a "can of worms" of
sorts, as these two groups do not agree.

Regards, John

Re: Proposal for new package group: Development:Formal Methods T

By Bill Nottingham at 08/26/2013 - 14:49

John C. Peterson (<a href="mailto: ... at eskimo dot com"> ... at eskimo dot com</a>) said:
Nothing of consequence (*) uses the RPM group tag any more, so I wouldn't
worry about that.

With respect to your particular definition of a comps group, you're creating
a large group with almost no default packages and a bunch of optional ones.

This sort of group definition is not the most useful, given that in the
installer (and with groupinstall) you'd only get the very small set of
packages (which may or may not be useful in isolation), and in other
post-install package tools, you'd be picking optional packages one at a
time.

How do you expect people to install these packages, and in what
combinations?

Bill

(*) I'm sure someone will mention something now

Proposal for new package group: Development:Formal Methods Tools

By John C. Peterson at 08/26/2013 - 17:31

On Mon, Aug 26, 2013 at 02:49:00PM -0400, Bill Nottingham wrote:
In my mind, the primary issued being addressed by adding the new group
is that these packages are currently in a group where *most* end users
would not expect to find them (Engineering and Scientific). That group
also has *many* packages in it, so some users may not notice them if
they are not paying attention.

FWIW, *all* of the packages I listed that are already listed in the
"Engineering and Scientific" group are currently optional packages.

For those user's who are knowledgable in Formal Methods, they will likely
know what they want and what they don't need. For those users who are
unfamiliar with such tools, they get a few packages to explore without
a lot of duplication of basic capability (e.g. there are multiple SAT
solvers).

Re: Proposal for new package group: Development:Formal Methods T

By Matthew Miller at 08/26/2013 - 15:01

On Mon, Aug 26, 2013 at 02:49:00PM -0400, Bill Nottingham wrote:
Maybe what would actually be most useful is to tag the related packages with
something ("formal methods"?) in <a href="https://apps.fedoraproject.org/tagger/" title="https://apps.fedoraproject.org/tagger/">https://apps.fedoraproject.org/tagger/</a>.

I'm not sure this is actually used by anything yet, but it's more likely to
be useful in the future than Groups or Comps, and the more useful data
that's there, the more likely that is.

Re: Proposal for new package group: Development:Formal Methods T

By Jerry James at 08/22/2013 - 17:26

On Sat, Aug 17, 2013 at 1:31 PM, John C. Peterson < ... at eskimo dot com> wrote:
I maintain or comaintain a fair number of these packages. I
originally added them to comps under "Engineering and Scientific",
just because there was no other category that was even remotely close
to what these packages do. However, they are not really a great fit
for that category. I like John's proposal. We should probably move
all of them over to this new category once it is created. We can
consider whether some of them should be listed in both places, but I
think most would be in the new formal-methods-tools category only.

Proposal for new package group: Development:Formal Methods Tools

By John C. Peterson at 08/24/2013 - 01:15

On Thu, Aug 22, 2013 at 03:26:48PM -0600, Jerry James wrote:
I think most users who are familiar with development tools based on Formal
proof methods would look for them under the "Development" category. (So I
agree, most all of the above packages should be moved into the new group).

The polybori, polybori-gui, polybori-ipbori packages certainly seem
like they could be meaningfully listed in both groups. (The provers
based on first order logic like the prover9, prover9-devel packages
seem like candidates as well, since they could be of interest to pure
mathematicians).