[Bug 1399366] New: Review Request:
prooftree - Proof tree visualization for Proof General
by Red Hat Bugzilla
https://bugzilla.redhat.com/show_bug.cgi?id=1399366
Bug ID: 1399366
Summary: Review Request: prooftree - Proof tree visualization
for Proof General
Product: Fedora
Version: rawhide
Component: Package Review
Severity: medium
Priority: medium
Assignee: nobody(a)fedoraproject.org
Reporter: loganjerry(a)gmail.com
QA Contact: extras-qa(a)fedoraproject.org
CC: package-review(a)lists.fedoraproject.org
Spec URL: https://jjames.fedorapeople.org/prooftree/prooftree.spec
SRPM URL:
https://jjames.fedorapeople.org/prooftree/prooftree-0.12-1.fc26.src.rpm
Description: Prooftree is a program for proof-tree visualization during
interactive
proof development in a theorem prover. It is currently being developed
for Coq and Proof General. Prooftree helps against getting lost between
different subgoals in interactive proof development. It clearly shows
where the current subgoal comes from and thus helps in developing the
right plan for solving it.
Prooftree uses different colors for the already proven subgoals, the
current branch in the proof and the still open subgoals. Sequent texts
are not displayed in the proof tree itself, but they are shown as a
tool-tip when the mouse rests over a sequent symbol. Long proof
commands are abbreviated in the tree display, but show up in full length
as tool-tip. Both, sequents and proof commands, can be shown in the
display below the tree (on single click) or in a separate window (on
double or shift-click).
Prooftree can mark the proof command that introduced a certain
existential variable and thus help to locate the problem when Coq says:
No more subgoals but non-instantiated existential variables
Fedora Account System Username: jjames
--
You are receiving this mail because:
You are on the CC list for the bug.
You are always notified about changes to this product and component
7 years, 4 months