Paperproof Extension Not Functioning Within Cursor

[Oren-H]

I ran into a lot of issues using Paperproof within the Cursor IDE. Cursor is a Fork of VS Code and extensions built for VS Code usually work in Cursor. I repeatedly ran into the error message "Missing "import Paperproof" in this .lean file, please import it." Switching to VS Code worked. I'm wondering if its possible to use Paperproof within Cursor.

[lakesare]

Both authors used it within Cursor, so this might be a recent issue

[Oren-H]

Oh strange. I tried several solutions (rebuilding lake file, restarting server, disabling/enabling extension, etc.) and nothing seemed to work. If anyone else has run into this issue with the current version of Paperproof and Cursor and has discovered a solution, that would be greatly appreciated.