Lake Manifest

The data structure of a Lake manifest and the definitions needed to create, modify, serialize, and deserialize it.

@[inline]

def Lake.Manifest.version : StdVer

The current version of the manifest format.

Three-part semantic versions were introduced in v1.0.0. Major version increments indicate breaking changes (e.g., new required fields and semantic changes to existing fields). Minor version increments (after 0.x) indicate backwards-compatible extensions (e.g., adding optional fields, removing fields).

Lake supports reading manifests with versions that have - suffixes. When checking for version compatibility, Lake expects a manifest with version x.y.z-foo to have all the features of the official manifest version x.y.z. That is, Lake ignores the - suffix.

VERSION HISTORY

v0.x.0 (versioned by a natural number)

• 1: First version
• 2: Adds optional inputRev package entry field
• 3: Changes entry to inductive (with path/git)
• 4: Adds required packagesDir manifest field
• 5: Adds optional inherited package entry field (and removed opts)
• 6: Adds optional package root name manifest field
• 7: type refactor, custom to/fromJson

v1.x.x (versioned by a string)

• "1.0.0": Switches to a semantic versioning scheme
• "1.1.0": Add optional scope package entry field

inductive Lake.PackageEntryV6 : Type

Manifest version 0.6.0 package entry. For backwards compatibility.

• path (name : Lean.Name) (opts : Lean.NameMap String) (inherited : Bool) (dir : System.FilePath) : PackageEntryV6
• git (name : Lean.Name) (opts : Lean.NameMap String) (inherited : Bool) (url rev : String) (inputRev? : Option String) (subDir? : Option System.FilePath) : PackageEntryV6

instance Lake.instFromJsonPackageEntryV6 : Lean.FromJson PackageEntryV6

instance Lake.instToJsonPackageEntryV6 : Lean.ToJson PackageEntryV6

instance Lake.instInhabitedPackageEntryV6 : Inhabited PackageEntryV6

inductive Lake.PackageEntrySrc : Type

The package source for an entry in the manifest. Describes exactly how Lake should materialize the package.

• path (dir : System.FilePath) : PackageEntrySrc

  A local filesystem package. dir is relative to the package directory of the package containing the manifest.

• git (url rev : String) (inputRev? : Option String) (subDir? : Option System.FilePath) : PackageEntrySrc

  A remote Git package.

instance Lake.instInhabitedPackageEntrySrc : Inhabited PackageEntrySrc

structure Lake.PackageEntry : Type

An entry for a package stored in the manifest.

• name : Lean.Name
• scope : String
• inherited : Bool
• configFile : System.FilePath
• manifestFile? : Option System.FilePath
• src : PackageEntrySrc

instance Lake.instInhabitedPackageEntry : Inhabited PackageEntry

def Lake.PackageEntry.toJson (entry : PackageEntry) : Lean.Json

instance Lake.PackageEntry.instToJson : Lean.ToJson PackageEntry

def Lake.PackageEntry.fromJson? (json : Lean.Json) : Except String PackageEntry

instance Lake.PackageEntry.instFromJson : Lean.FromJson PackageEntry

@[inline]

def Lake.PackageEntry.setInherited (entry : PackageEntry) : PackageEntry

@[inline]

def Lake.PackageEntry.setConfigFile (path : System.FilePath) (entry : PackageEntry) : PackageEntry

@[inline]

def Lake.PackageEntry.setManifestFile (path? : Option System.FilePath) (entry : PackageEntry) : PackageEntry

@[inline]

def Lake.PackageEntry.inDirectory (pkgDir : System.FilePath) (entry : PackageEntry) : PackageEntry

def Lake.PackageEntry.ofV6 : PackageEntryV6 → PackageEntry

structure Lake.Manifest : Type

Manifest data structure that is serialized to the file.

• name : Lean.Name
• lakeDir : System.FilePath
• packagesDir? : Option System.FilePath
• packages : Array PackageEntry

def Lake.Manifest.addPackage (entry : PackageEntry) (self : Manifest) : Manifest

Add a package entry to the end of a manifest.

def Lake.Manifest.toJson (self : Manifest) : Lean.Json

instance Lake.Manifest.instToJson : Lean.ToJson Manifest

def Lake.Manifest.getVersion (obj : JsonObject) : Except String SemVerCore

def Lake.Manifest.getPackages (ver : StdVer) (obj : JsonObject) : Except String (Array PackageEntry)

def Lake.Manifest.fromJson? (json : Lean.Json) : Except String Manifest

instance Lake.Manifest.instFromJson : Lean.FromJson Manifest

def Lake.Manifest.parse (data : String) : Except String Manifest

Parse a Manifest from a string.

def Lake.Manifest.load (file : System.FilePath) : IO Manifest

Parse a manifest file.

def Lake.Manifest.load? (file : System.FilePath) : IO (Option Manifest)

Parse a manifest file. Returns none if the file does not exist. Errors if the manifest is ill-formatted or the read files for other reasons.

def Lake.Manifest.save (self : Manifest) (manifestFile : System.FilePath) : IO PUnit

Serialize the manifest to a JSON file.

@[reducible, inline, deprecated Lake.Manifest.save (since := "2024-12-17")]

abbrev Lake.Manifest.saveToFile (self : Manifest) (manifestFile : System.FilePath) : IO PUnit

def Lake.Manifest.decodeEntries (data : Lean.Json) : Except String (Array PackageEntry)

Deserialize package entries from a (partial) JSON manifest.

def Lake.Manifest.parseEntries (data : String) : Except String (Array PackageEntry)

Deserialize manifest package entries from a JSON string.

def Lake.Manifest.loadEntries (file : System.FilePath) : IO (Array PackageEntry)

Deserialize manifest package entries from a JSON file.

def Lake.Manifest.tryLoadEntries (file : System.FilePath) : IO (Array PackageEntry)

Deserialize manifest package entries from a JSON file. Returns an empty array if the file does not exist.

def Lake.Manifest.saveEntries (file : System.FilePath) (entries : Array PackageEntry) : IO PUnit

Serialize manifest package entries to a JSON file.