def ImportGraph.Lake.Workspace.computeInputHash (ws : Lake.Workspace) : IO Lake.Hash

Computes the hash for the given workspace to persist in the summary. This should agree with the recomputed hash from the workspace summary if no changes are made to the package configuration.

Equations

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

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.

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.

def ImportGraph.Lake.WorkspaceSummary.ofWorkspace (ws : Lake.Workspace) (version : Option Lake.ToolchainVer) (inputHash : Lake.Hash) : WorkspaceSummary

Summarize a loaded Lake.Workspace for transport over Json.

Equations

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