lean3
lean3 copied to clipboard
leanprover
Search command
I'd like something like Coq's Search or SearchAbout: something that lists all of the theorems currently imported/accessible that match a particular pattern, and their types. (Apologies if something like this already exists, and I just didn't manage to find it.)
Is PR #1595 what you're looking for, or do you want something more sophisticated?
That'd be a good first step, if it's accessible in the emacs mode, and assuming I can get it to give me all the lemmas (search on the empty string?). I'd also like something more sophisticated: the ability to filter such a list by types, e.g., "give me all lemmas whose type mentions list" or "give me all lemmas of shape _ + (_ + _) = (_ + _) + _".
We recently met with a UW undergrad who was interested in implementing a SearchAbout/Hoogle/etc style feature for doing pattern & type based search. I'll check in with him this week and see if he has made any progress.
@gebner Suppose we have a #search command with the following features:
- We can specify constants that must appear in the type (e.g.,
list). - Patterns that must appear in the type (e.g.,
_ + (_ + _) = (_ + _) + _). - Identifier fragments (i.e., PR #1595). Would you have time to expose this feature on the Lean server/Emacs/VS Code?
@leodemoura Some server and vscode integration is already there, see #1595. On the emacs side, it shouldn't be too hard to add a search command via helm. The most difficult question is probably the choice of the keybinding. :smile:
There is one major design constraint to keep in mind with vscode (and other language-server-based editors):
- The built-in search command does not know what file we're in.
Right now, we search all loaded modules. If we use the search command to navigate, then I think this is the correct behavior. I want to navigate both "backwards" and "forwards".
Even if you're looking for lemmas to use in a proof, it might make sense to show them also if there are not imported yet.
Right now, we search all loaded modules. If we use the search command to navigate, then I think this is the correct behavior. I want to navigate both "backwards" and "forwards".
I agree. Isabelle searches backwards from the current location, which I found very annoying.
Even if you're looking for lemmas to use in a proof, it might make sense to show them also if there are not imported yet.
I agree this is useful. What would be the scope?
We could use the whole stdlib and all dependent packages listed in the configuration file.
What would be the scope?
Ideally, all the modules in the current package + dependencies (i.e. including the whole stdlib of course).
Practically speaking, this probably means "all modules that are in the module_mgr" (we could preload all available olean files to have everything available). One big issue is that we discard the produced environments on invalidation, and I'm not sure how much memory we would use if we kept them. We also don't produce environments for loaded olean files, so they're not really searchable. All of this assumes that we'd search by going through the environment.