Documentation

ImportGraph.Shake.Environment

Import hierarchy from the Environment #

This file takes an orthogonal approach to interacting with an import hierarchy than WorkspaceModel: namely, it builds a similar shake-style import hierarchy by looking at the imports in the Environment.

However, this is (1) insufficient in general (2) tricky, since there are divergences between which imports are loaded in the language server vs. with lake build. Likewise, imports of imports are not guaranteed to have data associated with them.

Yet, it is still useful for small commands which only need to inspect a local view of imports, and do not need to cross module system barriers in the import hierarchy under lake build (in which case higher modules will not be loaded, e.g. if they are privately imported). Interacting with the environment is faster than constructing a workspace model, so this is preferable in the simple cases it can work for.

It is therefore the case that this API should never be used while using WorkspaceModels. The ModIdx of a WorkspaceModel out of which we build a Needs has no connection to the ModuleIdx in an Environment out of which we'd build the same Needs.

source
def ImportGraph.Shake.Lean.Environment.transitiveClosureOf (env : Lean.Environment) (imps : Array Lean.Import) (transDeps : ArrayHierarchy) (base : Provides := Needs.empty) :
Provides

Computes the transitive closure of a set of imports with respect to an import hierarchy transDeps, as far as the environment allows.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[inline]
    def ImportGraph.Shake.Lean.Environment.currentTransNeeds (env : Lean.Environment) (transDeps : ArrayHierarchy) (excluding : Lean.NameSet := ∅) :
    Provides

    The current transitive imports as they are provided to the current environment.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def ImportGraph.Shake.Lean.Environment.mkTransDeps (env : Lean.Environment) :
      ArrayHierarchy

      Creates an Array Needs of transitive dependencies among modules present in the environment. Assumes that modules in the environment are topologically sorted.

      Caution: Lean imports more modules when in the language server than during a typical lake build. As such, this should only be used in cases where Needs information for the modules guaranteed to be present in the environment during build is sufficient, or else behavior should be gated on the value of the option Elab.inServer.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def ImportGraph.Shake.Lean.Environment.toRawImports (env : Lean.Environment) (n : Needs) (skipInit : Bool := true) :
        Array Lean.Import

        Assuming that the indices in Needs correspond to module indices in the provided environment, record an Import for each set index in Needs in some order. Note that this should not be used in tandem with a WorkspaceModel,which uses different indices for modules than those used in the environment.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def ImportGraph.Shake.Lean.Environment.toSimultaneousImportNeeds (env : Lean.Environment) (declNeeds : DeclNeeds) (declImportNeeds : ImportNeeds := ∅) :
          StanceM ImportNeeds

          Like DeclNeeds.toSimultaneousImportNeeds, but uses the environment's notion of ModuleIdx instead of a workspace model's.

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