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
<jcp(a)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:jcp@eskimo.com
San Diego, CA U.S.A