Transporting a Lake workspace summary over Json

This file defines WorkspaceSummary for summarizing a Lake workspace and getWorkspaceSummary for transporting the bare minimum over a process boundary. (This is then used to compute a WorkspaceModel, including import hierarchy data, with getWorkspaceModel from ImportGraph.WorkspaceModel.Build.)

The motivation for this is the need to inspect the broader import hierarchy and lake workspace from within the language server. However, loading the lake workspace from within the lake language server causes a crash, so we must call out to an exe (import-graph-workspace-summary) across a process boundary, and have it send back this data as json, which we then use (within the language server) to compute the much richer WorkspaceModel.

getWorkspaceSummary also caches the resulting json in the .lake folder to avoid future external calls if possible. Note that the module set is not included in the transported or cached json; these are recomputed from the roots and globs stored in the json.

This shares BaseWorkspace with WorkspaceModel.

@[reducible, inline]

abbrev ImportGraph.Lake.LibrarySummary : Type

A summary of lean_lib data for transport over Json.

Equations

• ImportGraph.Lake.LibrarySummary = ImportGraph.Lake.BaseLibrary

structure ImportGraph.Lake.PackageSummaryextends ImportGraph.Lake.BasePackage : Type

A summary of a lake package for transport over Json. All paths are absolute.

• baseName : Lean.Name
• origName : Lean.Name
• wsIdx : Nat
• dir : System.FilePath
• leanLibDir : System.FilePath
• deps : Array Nat

  The Lake indices of the package's direct dependencies (Lake's depPkgs).

• libs : Array LibrarySummary

  The package's lean_libs.

• configFile : System.FilePath

  The package's config file (absolute). We use this (only) for hashing.

def ImportGraph.Lake.instToJsonPackageSummary.toJson : PackageSummary → Lean.Json

Equations

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

@[instance_reducible]

instance ImportGraph.Lake.instToJsonPackageSummary : Lean.ToJson PackageSummary

Equations

• ImportGraph.Lake.instToJsonPackageSummary = { toJson := ImportGraph.Lake.instToJsonPackageSummary.toJson }

def ImportGraph.Lake.instFromJsonPackageSummary.fromJson : Lean.Json → Except String PackageSummary

Equations

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

@[instance_reducible]

instance ImportGraph.Lake.instFromJsonPackageSummary : Lean.FromJson PackageSummary

Equations

• ImportGraph.Lake.instFromJsonPackageSummary = { fromJson? := ImportGraph.Lake.instFromJsonPackageSummary.fromJson }

@[instance_reducible]

instance ImportGraph.Lake.instReprPackageSummary : Repr PackageSummary

Equations

• ImportGraph.Lake.instReprPackageSummary = { reprPrec := ImportGraph.Lake.instReprPackageSummary.repr }

def ImportGraph.Lake.instReprPackageSummary.repr : PackageSummary → Nat → Std.Format

Equations

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

@[instance_reducible]

instance ImportGraph.Lake.instInhabitedPackageSummary : Inhabited PackageSummary

Equations

• ImportGraph.Lake.instInhabitedPackageSummary = { default := ImportGraph.Lake.instInhabitedPackageSummary.default }

structure ImportGraph.Lake.WorkspaceSummaryextends ImportGraph.Lake.BaseWorkspace : Type

A summary of the lake workspace suitable for transport over Json. This may be obtained with getWorkspaceSummary and enriched into a model of the workspace and its intradependencies via getWorkspaceModel.

• dir : System.FilePath
• sysroot : System.FilePath
• leanLibDir : System.FilePath
• lakeSrcDir : System.FilePath
• leanSrcDir : System.FilePath
• version : Option Lake.ToolchainVer
• leanGitHash : String
• manifestFile : System.FilePath
• packages : Array PackageSummary

  The packages of the workspace, in Lake's workspace order (root first); each package's position is its lakeIdx.

• inputHash : UInt64

  The hash of inputs to this workspace summary: the lakefile (and the lakefiles of required packages), the lake manifest, the package-overrides.json, the lean-toolchain file, and the lean githash.

  We unwrap lake's Hash into a UInt64 to avoid a public lake dependency.

• packageOverridesFile : System.FilePath

  The .lake/package-overrides.json filepath (absolute). May not exist.

@[instance_reducible]

instance ImportGraph.Lake.instToJsonWorkspaceSummary : Lean.ToJson WorkspaceSummary

Equations

• ImportGraph.Lake.instToJsonWorkspaceSummary = { toJson := ImportGraph.Lake.instToJsonWorkspaceSummary.toJson }

def ImportGraph.Lake.instToJsonWorkspaceSummary.toJson : WorkspaceSummary → Lean.Json

Equations

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

def ImportGraph.Lake.instFromJsonWorkspaceSummary.fromJson : Lean.Json → Except String WorkspaceSummary

Equations

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

@[instance_reducible]

instance ImportGraph.Lake.instFromJsonWorkspaceSummary : Lean.FromJson WorkspaceSummary

Equations

• ImportGraph.Lake.instFromJsonWorkspaceSummary = { fromJson? := ImportGraph.Lake.instFromJsonWorkspaceSummary.fromJson }

@[instance_reducible]

instance ImportGraph.Lake.instReprWorkspaceSummary : Repr WorkspaceSummary

Equations

• ImportGraph.Lake.instReprWorkspaceSummary = { reprPrec := ImportGraph.Lake.instReprWorkspaceSummary.repr }

def ImportGraph.Lake.instReprWorkspaceSummary.repr : WorkspaceSummary → Nat → Std.Format

Equations

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

@[instance_reducible]

instance ImportGraph.Lake.instInhabitedWorkspaceSummary : Inhabited WorkspaceSummary

Equations

• ImportGraph.Lake.instInhabitedWorkspaceSummary = { default := ImportGraph.Lake.instInhabitedWorkspaceSummary.default }

def ImportGraph.Lake.WorkspaceSummary.exeName : String

The name of the executable with root ImportGraph.WorkspaceModel.Emit. Should be synchronized with the lakefile.

Equations

• ImportGraph.Lake.WorkspaceSummary.exeName = "import-graph-workspace-summary"

def ImportGraph.Lake.lakeDirPath (wsDir : Option System.FilePath) : IO System.FilePath

The "obvious" lakeDir given a workspace directory. TODO: Really, we ought to read this off of the lakeDir field from the lake-manifest.json instead of just trying to append .lake.

Equations

• ImportGraph.Lake.lakeDirPath wsDir = do let __do_lift ← wsDir.getDM IO.currentDir pure (__do_lift / { toString := ".lake" })

def ImportGraph.Lake.importGraphBuildDirPath (lakeDir : System.FilePath) : System.FilePath

A (new) folder in the given .lake directory for storing import graph data.

Equations

• ImportGraph.Lake.importGraphBuildDirPath lakeDir = lakeDir / { toString := "importGraph" }

def ImportGraph.Lake.WorkspaceSummary.cacheDirPath (lakeDir : System.FilePath) : System.FilePath

The directory in which the cache lives. This is currently importGraphBuildDirPath := .lake/importGraph/, a directory exclusively for special import graph data such as the workspace summary cache.

Equations

• ImportGraph.Lake.WorkspaceSummary.cacheDirPath = ImportGraph.Lake.importGraphBuildDirPath

def ImportGraph.Lake.WorkspaceSummary.cachePath (cacheDir : System.FilePath) : System.FilePath

Given a special-purpose build folder in the lake directory, the path to workspace-summary.json, where we cache the workspace summary.

Equations

• ImportGraph.Lake.WorkspaceSummary.cachePath cacheDir = cacheDir / { toString := "workspace-summary.json" }