On Thu, Aug 22, 2013 at 03:26:48PM -0600, Jerry James wrote: > On Sat, Aug 17, 2013 at 1:31 PM, John C. Peterson <j...@eskimo.com> wrote: > > 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 > > 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.
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). -- John C. Peterson, KD6EKQ mailto:j...@eskimo.com San Diego, CA U.S.A -- devel mailing list devel@lists.fedoraproject.org https://admin.fedoraproject.org/mailman/listinfo/devel Fedora Code of Conduct: http://fedoraproject.org/code-of-conduct
