Zulip Chat Archive

Stream: lean-gptf

Topic: Feature requests


view this post on Zulip Jesse Michael Han (Jan 18 2021 at 17:06):

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!

view this post on Zulip Bryan Gin-ge Chen (Jan 19 2021 at 02:32):

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.

view this post on Zulip Jesse Michael Han (Jan 19 2021 at 04:03):

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)


Last updated: May 18 2021 at 10:14 UTC