#find_home for ...

This module provides the #find_home for <cmd> utility, which suggests the highest places a given command (and its dependencies from the current file) can live in the import hierarchy. #find_home respects the module system.

Future work

UI

• Provide more information about the extracted dependencies of the given commands and declarations (e.g. why certain imports are necessary, what role certain declarations play). This information is available internally and needs only to be rendered helpfully.
• Provide more ranking options by default, and broadly improve the UI to be more informative (may involve moving off of MessageData to HTML)
• In the other direction, provide an "agent mode" that emits simplified textual information
• Provide more visibility into the import hierarchy. This may also be in the remit of related UX instead of #find_home per se.
• Take user to top of file instead of end when no declarations are present in the file

Functionality

• Handle non-modules
• Better errors; gracefully ignoring broken modules
• Provide a simplified meta API for accessing #find_home's composed functionality.
• Allow finding homes for commands which do not produce declarations
• Provide better support for moving declarations with same-file dependencies:
  • Capture the syntax needs of dependencies, e.g. via a stateful linter
  • Allow copying all of the dependencies at once
• Capture and copy over scopes/namespaces.
• Optionally leave behind relocated ... to ... commands
• Handle meta definitions.
• Handle movements between libraries in the same package, and be more careful about labeling other packages as "upstream".
  • Currently #find_home makes the simplifying assumptions that you do not want to move code laterally to other libraries in the same package, and that all other packages in the workspace are "upstream."
  • Similarly, make the allowed target locations configurable somehow (see below).
  • Also allow non-default targets.
• Allow for "mutation": find near-misses, where slight alterations to (1) the import hierarchy or (2) aspects of the current commands might allow other "homes" to be found.
• Allow for configurable queries, which could express e.g. e.g. "only consider modules which don't import <module A>" or "only consider modules downstream/upstream of <certain set of modules>" or "minimize the (nonzero) amount of category theory imported"
  • Handle configurable export preservation (e.g. "the highest place which provides this to <module>")

def ImportGraph.Shake.findHomeStx : Lean.ParserDescr

⚠️ #find_home is currently experimental. Please report any wish-list features, possible ergonomic improvements, or errors on GitHub or Zulip.

---

#find_home for <cmd> finds the highest modules in the import hierarchy in which <cmd> (and the declarations produced during it) can live. This accounts for the syntax, constants, and executable code produced during <cmd>, and respects the module system.

This includes any declarations which are dependencies of <cmd> from the current file, which should be moved along with it. (Currently, #find_home does not account for the syntax of those dependencies, nor does it suggest moving such dependencies individually.)

Note that #find_home may take a long time on its first run. It caches data about the module hierarchy both in the .lake folder and interactively to make subsequent runs faster.

Known limitations

• #find_home does not yet handle meta definitions.
• #find_home does not yet account for the syntax of dependent definitions.
• #find_home may not function correctly outside of the module system.
• For smaller miscellaneous limitations, see the module docstring.

Equations

• One or more equations did not get rendered due to their size.

Non-module #find_home

This code is a fallback since #find_home for does not yet work outside the module system.

def Lean.Name.findHome (n : Name) (env : Option Environment) : CoreM NameSet

Warning: this declaration does not respect the module system, and should only be used outside of it.

Find locations as high as possible in the import hierarchy where the named declaration could live.

def oldFindHomeStx : Lean.ParserDescr

#find_home <ident> is in the process of being deprecated. Instead, use

#find_home for
<command>

where <command> declares <ident>. This ensures that the imports necessary for the syntax and tactics used in the declaration are present too.

The following describes the functionality outside of the module system, which may not work:

Find locations as high as possible in the import hierarchy where the named declaration could live. Using #find_home! will forcefully remove the current file. Note that this works best if used in a file with import Mathlib.

The current file could still be the only suggestion, even using #find_home! lemma. The reason is that #find_home! scans the import graph below the current file, selects all the files containing declarations appearing in lemma, excluding the current file itself and looks for all least upper bounds of such files.

For a simple example, if lemma is in a file importing only A.lean and B.lean and uses one lemma from each, then #find_home! lemma returns the current file.

Equations

• One or more equations did not get rendered due to their size.