Documentation

ImportGraph.WorkspaceModel.Summary.Cache

Workspace summary cache validation #

Computes hashes from the paths stored in a workspace summary. This file does not import Lake workspace configuration or loading; extraction from a live workspace belongs in Summary.Lake.

source
def ImportGraph.Lake.computeInputHash (leanGitHash : String) (ver : Option Lake.ToolchainVer) (manifestFile packageOverridesFile : System.FilePath) (packageConfigs : Array System.FilePath) :
IO Lake.Hash

Internal helper shared by cache validation and the workspace-summary executable. Hashes the toolchain identity and workspace configuration files.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def ImportGraph.Lake.WorkspaceSummary.recomputedInputHash (leanGitHash : String) (ws : WorkspaceSummary) :
    IO Lake.Hash

    Recomputes the input hash for the WorkspaceSummary by re-hashing the files at the given paths. Also mixes in the hash for the given lean version.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def ImportGraph.Lake.WorkspaceSummary.isUpToDate (ws : WorkspaceSummary) (wsDir? : Option System.FilePath := none) :
      IO Bool

      Recomputes the hash of the data referred to by the paths in WorkspaceSummary and compares it to the hash in WorkspaceSummary, using the current lean process's git hash.

      If wsDir? is provided, ensures that the workspace directory provided in the summary is the same as the given wsDir, else considers it not up-to-date.

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