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.
Paths come from the repository package-file index for the observed builds. They describe archive/package associations, not every file that will exist on a running system after maintainer scripts, alternatives, generated state, diversions, or installation choices.
Each row is recorded package-index metadata for one version, architecture, suite, and repository. Names, URLs, and sizes are source-reported; a link is a potentially mutable retrieval location, not an OpenFactory redistribution claim or proof that OpenFactory retained the artifact bytes.
For an APT source, signature verification authenticates the repository metadata chain and the Packages index containing this source-reported artifact digest. It does not certify package safety.
0.14-10.fc44 / aarch64Observed Sep 1, 2026 to Sep 1, 2026
Verification status: Metadata observed; artifact bytes were not independently fetched or hashed by this catalog import. The digest below is source-reported.
0.14-10.fc44 / x86_64Observed Sep 1, 2026 to Sep 1, 2026
Verification status: Metadata observed; artifact bytes were not independently fetched or hashed by this catalog import. The digest below is source-reported.