[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

Re: Bug#672480: ITP: prooftree -- proof tree visualization for Proof General

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?

Kind regards



Reply to: