Skip to content

Paperproof 1.6.0

Latest
Latest
Compare
Choose a tag to compare
@lakesare lakesare released this 27 Aug 09:52
· 18 commits to main since this release
1.6.0
6fd11de

Overview

BEFORE AFTER
image image

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
    image image

  • 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
    image image

  • 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": ["leanprover.lean4@0.0.176", "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:

    Paperproof in codespaces

Changed

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

    BEFORE NOW
    image image

  • 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
    image image
    image image
Assets 2
Loading