PROOFTREE(1)

📦
version 0.14 · 2 versions
, in fedora 43, fedora 44, nixos 26.05

💖 PROOFTREE(1) 💖 — proof-tree display for Proof General

okay bestie, pull up a chair, we're reading the prooftree manual together and honestly?? it's giving iconic. It lives in the User Manuals section, and it's here to show you your proof trees while you're doing proof development with Proof General. 🎀

✨ NAME ✨

prooftree — proof-tree display for Proof General 🦋

🌸 SYNOPSIS 🌸

prooftree [Options...]

💅 DESCRIPTION 💅

So what does it actually do? Prooftree visualizes proof trees during proof development with Proof General. Right now it only works for Coq, though adding support for other proof assistants should be relatively easy. (ngl, that's a lil slay of whoever wrote it.)

To start a proof-tree display, hit the Prooftree icon in the Proof General tool-bar, or select the menu entry Proof-General -> Start/Stop Prooftree, or type C-c C-d (which runs proof-tree-external-display-toggle). Inside a proof, this will immediately start a proof-tree display for the current proof. Outside a proof, Proof General remembers to start the proof-tree display for the next proof. ✨

Under normal circumstances Prooftree is started by Proof General as an Emacs subprocess. The user interacts with Prooftree only through the graphical user interface. A substantial part of the proof-tree visualization task is done by Proof General. Therefore not only the Prooftree command line arguments but also other aspects can only be configured inside Proof General — see Proof General Customization below. 👑

🔥 OPTIONS 🔥

  • -help — Print synopsis and exit. Short, sweet, bye. 👋
  • -config — Open the configuration dialog on startup (if you want to change the configuration without starting Proof General). Very "let me fix my vibe first" of you.
  • -geometry spec — Sets the X geometry of the main window. spec is a standard X geometry string in the form xposxypos[+xoff[+yoff]]. 📐
  • -tee file — Write all input to file (usually for debugging purposes). It's the "record everything for the group chat" option fr fr.
  • -debug — Provide more details on errors. When things go 💀, this tells you why.
  • -help-dialog — Open the help dialog on startup. Mainly useful for proofreading the help text. 🎀
  • -test-coq-evar-parser data — Call the Coq evar parser on data, pretty print the result and exit. Useful for debugging the evar parser only. A lil specialist moment, we respect it.

🌈 MAIN PROOF DISPLAY 🌈

Prooftree opens one window for each proof that it is requested to display. This window contains the proof-tree graph and a small display for sequents and proof commands. Two-for-one, obsessed. 💖

🎨 Colors 🎨

The branches in the proof-tree graph are colored according to their state. Prooftree distinguishes between the following states.

  • current (blue by default) — The current branch is the branch from the root of the proof tree to the current goal. It's the main character, obviously. 👑
  • unproven (default foreground color) — A branch is unproven if it contains open proof goals. Not finished yet, no cap.
  • proved incomplete (cyan by default) — An incompletely proved branch has its proof finished, but some of the existential variables that have been introduced in this branch are not (yet) instantiated. So close bestie, so close 😭
  • proved partially (dark green by default) — In a partially proved branch all existential variables of the branch itself are instantiated, but some of those instantiations contain existential variables from other branches that are not (yet) instantiated. It's giving "I did my part, someone else didn't."
  • proved complete (green by default) — A branch is proved complete if all its existential variables are instantiated with terms that themselves do not contain any existential variables. Fully ate. ✅
  • cheated (red by default) — A cheated branch contains a cheating proof command, such as admit. Uh oh. We saw that. 🚨

The colors as well as many other Prooftree parameters can be changed in the Prooftree Configuration Dialog (see below). ✨

When the proof tree grows large one can navigate by a variety of means. In addition to scroll bars and the usual keys one can move the proof tree by dragging with mouse button 1 pressed. By default, dragging moves the viewport (i.e., the proof tree underneath moves in the opposite direction). After setting a negative value for Drag acceleration in the Prooftree Configuration Dialog, dragging will move the proof tree instead (i.e., the proof tree moves in the same direction as the mouse). 🖱️

📜 Sequent Display 📜

The sequent display below the proof tree normally shows the ancestor sequent of the current goal. With a single left mouse click one can display any goal or proof command in the sequent display. A single click outside the proof tree will switch back to default behavior. The initial size of the sequent display can be set in the Prooftree Configuration Dialog. A value of 0 hides the sequent display. 🫶

💬 Tool Tips 💬

Abbreviated proof commands and sequents are shown in full as tool tips when the mouse pointer rests over them. Both the tool tips for abbreviated proof commands and for sequents can be independently switched off in the Prooftree Configuration Dialog. The length at which proof commands are abbreviated can be configured as well. 👀

🪟 Additional Displays 🪟

A double click or a shift-click displays any goal or proof command in an additional window. These additional windows are automatically updated, for instance, if an existential variable is instantiated. For additional sequent displays one can browse the instantiation history of the sequent using the forward and backward buttons. These additional windows can be detached from the proof tree. A detached display is neither automatically updated nor automatically deleted. 🙈

🦋 Existential Variables 🦋

Prooftree keeps track of existential variables, whether they have been instantiated and whether they depend on some other, not (yet) instantiated existential. It uses different colors for proved branches that created currently not instantiated existential variables and branches that only depend on some not instantiated existential created in different branches. The list of currently not (yet) instantiated existential variables is appended to proof commands and sequents in tool-tips and the other displays. 🧚

The Existential Variable Dialog displays a table with all existential variables of the current proof and their dependencies. Each line of the table contains a button that marks the proof command that introduced this variable (with yellow background, by default) and, if present, the proof command that instantiated this variable (with orange background, by default). 🍊

The Menu button displays the main menu. The Clone item clones the current proof tree in an additional window. This additional window continues to display a snapshot of the cloned proof tree, no matter what happens with the original proof. Frozen in time, lowkey poetic.

The Show current and Show selected items move the viewport of the proof tree such that the current proof goal, or, respectively, the selected node will be visible (if they exist).

The Exit item terminates Prooftree and closes all proof-tree displays. 🚪

The remaining four items display, respectively, the Existential Variable Dialog, the Prooftree Configuration Dialog, and the Help and About windows.

🖱️ Context Menu 🖱️

A right click displays the Context Menu, which contains additional items.

The item Undo to point is active over sequent nodes in the proof tree. There, it sends an retract or undo request to Proof General that retracts the scripting buffer up to that sequent. ⏪

The items Insert command and Insert subproof are active over proof commands. They sent, respectively, the selected proof command or all proof commands in the selected subtree, to Proof General, which inserts them at point. ✍️

⚙️ CONFIGURATION ⚙️

💖 Prooftree Configuration Dialog 💖

The configuration dialog permits to change fonts, colors, layout parameters for proof tree drawing, to configure tool tips, initial window sizes and some other points. Changes in the configuration dialog take immediate effect. The Save button stores the current configuration (as marshaled OCaml record) in ~/.prooftree, which will overwrite the built-in default configuration for the following Prooftree runs. The Revert button loads and applies the saved configuration. The Cancel and OK buttons close the dialog, but Cancel additionally resets the configuration to the state before the start of the dialog. To avoid opening partial file names, the Log Proof General input check box is deactivated when typing the log file name. 🌸

🎀 Proof General Customization 🎀

The location of the Prooftree executable and the command line arguments are in the customization group proof-tree. Prover specific points, such as the regular expressions for navigation and cheating commands are in the customization group proof-tree-internals. To visit a customization group, type M-x customize-group followed by the name of the customization group inside Proof General. 💅

😭 LIMITATIONS 😭

In additional sequent displays, the information about existential variables is only shown for the latest version of the sequent and not for older versions in the instantiation history.

The synchronization between Proof General and Prooftree is not perfect. There are a few race conditions which are unlikely to occur during interactive proof development but can be triggered by asserting larger parts of a proof or by very quick user actions. Yes this is a real warning, bestie, read it.

  • In a situation, where a goal contains an existential variable, this variable is instantiated (in different branch of the proof), and the goal is shelved and quickly unshelved, it might happen that the updated sequent text (containing the instantiating of the existential variable) is associated with the unshelved version of the goal.
  • Spawned subgoals and the instantiating of existential variables cause asynchronous update-sequent messages sent to Prooftree. When quickly retracting portions of the proof, the corresponding undo message might overtake same update-sequent messages and thereby confuse Prooftree.

🧚 PREREQUISITES 🧚

This version of Prooftree requires Coq 8.11 or better and Proof General from March 2021 or later. No old vibes allowed. ✨

📁 FILES 📁

  • ~/.prooftree — Saved Prooftree configuration. Is loaded at application start-up for overwriting the built-in default configuration. Must contain a marshaled OCaml configuration record. 🎀

👀 SEE ALSO 👀

🕰️ HISTORY ✨

Okay so storytime bestie, because Prooftree's origin story is genuinely a journey. 💖

Prooftree was developed in 2011 to help keep orientation in larger Coq proofs, which, mood, because big proofs are a lot. The very first versions required patches for Coq — yes, actual patches, we were out here living dangerously. 🫠

Then at the third Coq workshop in Nijmegen, the Netherlands, also in 2011, there was a meeting with the Coq development team, and Arnaud Spiwack added the necessary support for Prooftree to Coq. Iconic behavior, no cap. 👑

And then, the glow-up: Prooftree version 0.8 was the first version that worked with Coq 8.4beta and the Proof General development version. We ate. 💅

But babes, it was not all smooth sailing. 😭 The user friendly names for existential variables, introduced in Coq 8.6, broke many Prooftree features for existential variables. Rude. And the removal of the Show Goal id command in Coq 8.7 broke Prooftree completely. Not "a little broken", not "quirky", just full-on 💀.

Then in 2019, Jim Fehrle added the necessary support for Prooftree again to Coq 8.11. The existential variable printout and the Show Goal command were slightly generalized, which made it possible to simplify the proof tree code in Proof General quite a bit. Cleanup arc, we love to see it. 🧚✨

💫 CREDITS 💫

Prooftree has been inspired by the proof tree display of PVS. Shoutout to the ancestors, fr fr. 🙌

👑 AUTHOR 👑

Hendrik Tews <prooftree at askra.de>

And that's the whole page, bestie! 🎀 This was the PROOFTREE(1) manual page, dated April 2020, and the source/version footer you'd normally see at the bottom was just PROOFTREE with the same April 2020 date and PROOFTREE(1) on the right. Go read some proof trees, you've got this. 🦋💜

📦 where this page comes from