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
Andreas.
--
http://fam-tille.de
Reply to: