Created a TUI (terminal-only) version of PaperProof

[wvhulle]

For the people, who do not want to VS Code, I created a TUI version. There are two display modes (switch with [/] that use PaperProof library underneath.

You see the docs on: https://codeberg.org/wvhulle/lean-tui

[antonkov]

Woah - so cool!! Thanks Willem!

[wvhulle]

Woah - so cool!! Thanks Willem!

Thanks. I am using your library for additional info about expressions and proof states. I noticed however I still need to assemble the DAG. Have you considered moving that logic from your Typescript code to Lean? Or did I look past it?

[antonkov]

I think it makes sense to have it calculated on the Lean side if you willing to contribute it as an option? :)

Historic remark on why it's not in Lean now:
Originally we were thinking to have a frontend code to be served dynamically from some site (e.g. paperproof.xyz) so that the proofs are persisted and can be shared. This design also would've allowed to iterate and change visualization quickly (just push new UI to a server) without requiring users to update lean package or VSCode extension. Which seemed valuable as we were expecting some iterations before we get the format right.

However after people started using it - turned out, that offline mode is more important and the visualization format wasn't changing much. So retrospectively having it as part of Lean library is more useful!

[wvhulle]

Even better would be to have it in Lean core right? Did someone ever try that?

[lakesare]

After we change the extension code (everything from /app and /extension), we can deploy the extension, and everyone who has a Paperproof vscode extension installed will see the updates immediatley, it's auto-updated.
If we change the Lean library code (everything from /lean), we push it to github, and people have to manually refetch the Lean library using lake update.
This means that everything written in Lean is much harder to update for the users. So we try not to touch the parser much, it's supposed to be minimal.

Another reason to keep the Lean portion of the codebase minimal is that nearly every time the new Lean version comes out, we have to update our accompanying Lean code. It's not just a matter of the development effort, it's a matter of how many people have Paperproof broken for their Lean version (the more Lean code, the greater the risk Paperproof breaks for different Lean versions).

So I'd rather try to keep /lean minimal.

[antonkov]

Put this way I think I agree with Evgenia, thanks for the refresher on painpoints and rationale :)

[wvhulle]

@lakesare why does the lean portion of the lib break with every new lean version? Isn’t it relatively low level stuff that shouldn’t change that much?

[lakesare]

@wvhulle, the code we use is considered internal-use, so its backwards compatibility isn't considered when Lean's minor version is bumped.
So nearly every update like 4.25.0 => 4.26.0 is a breaking change for us.

[wvhulle]

@wvhulle, the code we use is considered internal-use, so its backwards compatibility isn't considered when Lean's minor version is bumped.
So nearly every update like 4.25.0 => 4.26.0 is a breaking change for us.

Okay, that's strange. I thought there was more stability to these essential things?

[lakesare]

Heh there is very little stability to Lean in general at the moment, even stuff around Sets/Strings gets breaking changes regularly.