Build error in CheckIfUserIsStillTyping.lean

[RickDW]

Hiya,

I'm following the instructions provided by both Mathematics in Lean and Paperproof and it seems to be completely broken at the moment. After adding require Paperproof from git "https://github.com/Paper-Proof/paperproof.git"@"main"/"lean" to the lakefile.lean file, and import Paperproof to one of the .lean files, and then restarting the file as indicated by VS Code, I get the following error:

[1980/1980] Building Paperproof
Some build steps logged failures:
- Building CheckIfUserIsStillTyping
error: build failed

I have tried re-installing everything and have even wiped my entire set of elan toolchains but nothing seems to help. Can anyone here shed some light on this?

[lakesare]

Hi Rick!

Looks like the new Lean version breaks something in our CheckIfUserIsStillTyping.lean.

Can you take a look at what your Lean version is?

[RickDW]

Hi Evgenia! I'm running the very latest release candidate, v4.8.0-rc1, so that would explain the issue. Is there a workaround for this or should I just downgrade Lean for the time being?

Just as a quick aside, it might be worth updating the list of supported versions since Paperproof's Reservoir page lists this version as fully supported

[lakesare]

Is there a workaround for this or should I just downgrade Lean for the time being?

No easy workaround until we rewrite that portion of the code to be compatible with the new Lean, I'll try to look at it this weekend. Right now you can downgrade to Lean (version 4.0.0-nightly-2023-06-20, commit a44dd71ad62a, Release) - this is my version of Lean, and it was certainly working with Paperproof last time I checked.

[lakesare]

Made Paperproof work with leanprover/lean4:v4.8.0-rc1 (fixed in this commit). Just running lake update Paperproof should update Paperproof to the version that works with v4.8.0.

---

Latest Paperproof works with the following Lean versions:

• 4.0.0-nightly-2023-06-20
• v4.8.0-rc1

And I assume with everything in between (though I couldn't check that, switching Lean versions takes ~20 minutes even when everything goes smoothly).

---

Thanks for the report @RickDW, please feel free to reopen if you have some further issues.

[RickDW]

Thanks for the quick update! The error I saw has disappeared after I updated Paperproof, but it seems like something is still broken. All I can see in the Paperproof window inside VS Code is a completely white background. I'm not sure if this is related to the previous build error?

[lakesare]

Huh could reproduce it! I didn't have this error just two days ago, but I did get it today.

This needs further exploration, but what I believe happened is vscode-lean4 extension got updated in the past few days, bringing about the "asUri is not a function" error. Probably something related to this PR https://github.com/leanprover/vscode-lean4/pull/437. (To be clear - this is not a bug in vscode-lean4, it's a bug in how Paperproof interacts with vscode-lean4 - we depend on their inner apis that can change).

This can be fixed in the following way:

1. Follow these instructions to rollback lean4 extension to version v0.0.140.
2. Fully close vscode, open vscode.
3. Try opening Paperproof again.

[lakesare]

Made Paperproof work with the latest lean extension (vscode-lean4 v0.0.140).

Updating to vscode extension Paperproof v1.3.0 should fix the blank screen.

Again - thanks for the report!