Feature requests

Stream: lean-gptf

[Jesse Michael Han]

Planned features:

• special support for rw, simp
• special support for exact
• premise selection/lemma suggestion
• full push-button proof search (currently, gptf performs one-step lookahead on all the predictions returned by the model)
• support for running your own transformer language model locally

ideas welcome!

[Bryan Gin-ge Chen]

Would it be feasible to have some kind of caching mechanism for suggestions? Right now I can use vscode-lean's copy-to-comment button to put the suggestions in a comment, but this ends up modifying the Lean file, which then triggers the server to run gptf again. Maybe we should have the infoview handle this sort of thing.

[Jesse Michael Han]

Bryan Gin-ge Chen said:

Would it be feasible to have some kind of caching mechanism for suggestions? Right now I can use vscode-lean's copy-to-comment button to put the suggestions in a comment, but this ends up modifying the Lean file, which then triggers the server to run gptf again. Maybe we should have the infoview handle this sort of thing.

ah, it would be nice to have a custom interaction monad begin [gptf] ... end which runs a state_t search_state tactic --- then the user would be able to step through the entire breadth-first search, reorder the search queue, manually backtrack, look up previous predictions, etc.

the smt mode does a similar caching of ematch lemmas (indeed, the smt mode is just state_t smt_state tactic)