Interact with relp without project

[kaifronsdal]

Is there a simple way to interact with an empty project from lean-dojo without creating it from scratch? In other words, create a blank project from within lean-dojo with an empty file you can add your theorems/definitions/imports arbitrarily rather than using an already created project and referring to a theorem in a file.

It doesn't look like this functionality is implemented, but perhaps there is a way I can write a short wrapper to do this myself. One potential idea is to copy a blank project each time and use command mode to define a theorem and then switch to tactic mode as needed. Does anyone have any suggestions?

[yangky11]

Hi,

LeanDojo does not currently support it. I'd recommend two potential solutions:

1. Create a wrapper around https://github.com/lean-dojo/LeanDojo/blob/main/src/lean_dojo/interaction/Lean4Repl.lean
2. Use repl

Please feel free to let me know if you have further questions.