Paperproof v1.6.4

Overview

Changes that make working on real formalization projects with Paperproof easier.

Added

• Handle #exit gracefully
  If your cursor is placed after the #exit command, Paperproof will tell you about it.

  

Changed

• Removed floating hypotheses
  They were not working very well for large proofs.

• Made Paperproof NOT affect performance of the default InfoView
  Made it so that when the Paperproof panel is closed, rpc requests don't get sent (see #51).

• Easier text selection in goals and hypotheses
  Previously, when you tried selecting some text from the goal or a hypothesis node, Paperproof would zoom in on the box you clicked on. Now this zoom won't happen during the "select" motion.

Paperproof v1.6.0

Overview

BEFORE	AFTER

Added

• Added an option "Hide goal names"
  Goal names (see, for example, a grey box with "right.left" written on them) are immensely helpful during some types of proofs, for example when we do induction proofs about functions.
  In some proofs, however, goal names just clutter the interface, and it should be possible to hide them.
  From now on, we hide the goal names by default, in the spirit of making the initial interface perfectly intelligible to the Paperproof novice.

  Hide goal names: off	Hide goal names: on

• Added an option "Always green hypotheses"
  Again - this is to ease beginner's understanding of Paperproof proofs. Additional colors do ease the reading of a proof, but might be confusing initially. From now on, we let people turn on this functionality when they are ready for it.

  Always green hypotheses: off	Always green hypotheses: on

• Made it possible to render Paperproof in github codespaces

  Just go to github.com/codespaces/new/Paper-Proof/paperproof and wait for a few minutes for your codespace to load.
  That usually takes 2-4 minutes.
  If you have a Lean repo, and you would like to enable codespaces in it, all it takes is these two files: .devcontainer.
  If you would like to enable Paperproof in your codespaces, just add "extensions": ["[email protected]", "paperproof.paperproof"] (note that we fix the leanprover.lean4 extension version - this makes sure leanprover.lean4 extension updates don't break your codespace).

  Here is what it will look like:

  

Changed

• Changed the way initial hypotheses are displayed
  Previously we had a fake init tactic. Now, we changed it to "HYPOTHESES" header.

  BEFORE	NOW

• Changed the font and variable colors
  Here we both move towards and away from Lean's default InfoView.
  We changed our font to match the one Lean's InfoView uses - it renders mathematics symbols much more clearly than our previous font.
  On the other hand, we changed the variable color from the orange color (used in Lean's InfoView) to dark pink, which is easier to read on our green node backgrounds.

  BEFORE	NOW

Paperproof v1.0.0

Changes:

• Paperproof works offline now, too

• Tactic combinators get properly displayed

• Added various modes that change how the proof is displayed: compact mode, compact tactics mode, readonly mode
  

• Upon right-clicking on a particular box, you can collapse it now
  

• Hypotheses have grey, yellow, and green colors - grey ones is sorts which we do not show; yellow ones is data; green ones is proofs
  

In general - Paperproof was fully rewritten (we went from Tldraw to vanilla React). Interaction with Paperprooof feels different now, it's just a normal webpage that you can scroll around.

Paperproof v0.0.5

The first official release of Paperproof.