Re: Bug#672480: ITP: prooftree -- proof tree visualization for Proof General
On Mon, May 14, 2012 at 12:03:32PM +0200, Andreas Tille wrote:
> On Mon, May 14, 2012 at 10:52:28AM +0200, Hendrik Tews wrote:
> >
> > and tell us, in what task your package might fit best.
> >
> > If prooftree ever makes it into Debian, it should be together
> > with coq and proof-general, ie. science-mathematics.
>
> OK, thanks. I'll care for this.
>
> > BTW:
> > - matita, agda, prover9 are proof assistants similar to coq, but
> > not listed in science-mathematics
> > - hol-light, currently waiting in the new-queue, too
>
> I will add all these - new is regarded in the tasks generation script
> as well.
>
> > - minisat would also belong to this group
> > - you might want to have a separate meta-package
> > "theorem-proving" or "formal-methods" for all these tools
>
> This kind of input is exactly what is wanted here on this list.
>
> Regarding the split into separate meta-packages: While I agree that
> science-mathematics becomes a bit crowded I'm not fully sure that we
> should keep on maintaining mathematical packages under the Debian
> Science umbrella. I'd rather vote for some math-* tasks which enables
> mor fine grained tasks (same probably for physics).
>
> Any opinions?
ScienceLogic [1] would be more appropriate, IMHO, in particular when
ScienceMathematics is getting crowded.
[1] http://wiki.debian.org/DebianScience/Logic
-Ralf.
Reply to: