Paperproof v2.0.0

Overview

This release introduces an experimental UI for Lean 4: a Single-Tactic Mode.

Single-Tactic Mode is primarily useful during the process formalization. This mode works well on proofs of any size, and shows all information the default InfoView might show.

This UI is very similar to the default InfoView, with one important distinction - instead of showing the diff (by highlighting the substrings of the hypothesis/goal that changes), we simply display the "before" and the "after" types, one below the other.

The usual paperproof niceties stay around too - hypotheses are color-coded (proof vs data), hypotheses that were used by the tactic are highlighted, and you can see the used theorem's signature side-by-side to pattern match it to the effect the tactic took.

Essentially, this interface is meant to shorten the repetitive action of "click on the line before the tactic; click on the line after the tactic; hover over the theorem definition" - a single click on the tactic line should suffice to understand what exactly this tactic line is doing.

Added

• New UI mode: "Single-Tactic Mode"

  Notice how a cursor set at rw [Set.mem_inter_iff, and_comm] at h1 only displays the effect the rw created, ignoring the rest of the proof.

  

  All theorem names present in a tactic are underlined. When you click on the theorem name, you can see that theorem's signature:

  

• New context menu action: "Hide hypothesis"

  In both modes, you can now hide a bulky hypothesis node by right-clicking on it and selecting "Hide hypothesis".

  

• Logs for LLMs

  If you'd like your llm to quickly understand the structure of some proof, you can CMD+SHIFT+P: Open Webview Developer Tools, click within some proof, and copypaste the console.logged valued called "copypaste". Per each tactic, it will produce the following output:

  tactics: [ 
   ...,
   {
     text: "intro h1",
     hypothesisChanges: [{ from: null, to: ["x ∈ s ∩ t"] }],
     goalChanges: [{ from: "x ∈ s ∩ t → x ∈ t ∩ s", to: "x ∈ t ∩ s" }],
     closedSomeGoal: null
   },
   ...
  ]
  

  This makes use of Paperproof's diffing algorithm, the output only contains the parts that were indeed changed by the tactic.