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

Equations

• Lake.Manifest.version = { major := 1, minor := 1 }

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

Equations

• Lake.instFromJsonPackageEntryV6 = { fromJson? := Lake.fromJsonPackageEntryV6✝ }

instance Lake.instToJsonPackageEntryV6 : Lean.ToJson PackageEntryV6

Equations

• Lake.instToJsonPackageEntryV6 = { toJson := Lake.toJsonPackageEntryV6✝ }

instance Lake.instInhabitedPackageEntryV6 : Inhabited PackageEntryV6

Equations

• Lake.instInhabitedPackageEntryV6 = { default := Lake.PackageEntryV6.path default default default default }

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

Equations

• Lake.instInhabitedPackageEntrySrc = { default := Lake.PackageEntrySrc.path default }

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

Equations

• Lake.instInhabitedPackageEntry = { default := { name := default, scope := default, inherited := default, configFile := default, manifestFile? := default, src := default } }

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

Equations

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

instance Lake.PackageEntry.instToJson : Lean.ToJson PackageEntry

Equations

• Lake.PackageEntry.instToJson = { toJson := Lake.PackageEntry.toJson }

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

Equations

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

instance Lake.PackageEntry.instFromJson : Lean.FromJson PackageEntry

Equations

• Lake.PackageEntry.instFromJson = { fromJson? := Lake.PackageEntry.fromJson? }

@[inline]

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

Equations

• entry.setInherited = { name := entry.name, scope := entry.scope, inherited := true, configFile := entry.configFile, manifestFile? := entry.manifestFile?, src := entry.src }

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

def Lake.PackageEntry.ofV6 : PackageEntryV6 → PackageEntry

Equations

• Lake.PackageEntry.ofV6 (Lake.PackageEntryV6.path a a_1 a_2 a_3) = { name := a, inherited := a_2, src := Lake.PackageEntrySrc.path a_3 }
• Lake.PackageEntry.ofV6 (Lake.PackageEntryV6.git a a_1 a_2 a_3 a_4 a_5 a_6) = { name := a, inherited := a_2, src := Lake.PackageEntrySrc.git a_3 a_4 a_5 a_6 }

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.

Equations

• Lake.Manifest.addPackage entry self = { name := self.name, lakeDir := self.lakeDir, packagesDir? := self.packagesDir?, packages := self.packages.push entry }

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

Equations

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

instance Lake.Manifest.instToJson : Lean.ToJson Manifest

Equations

• Lake.Manifest.instToJson = { toJson := Lake.Manifest.toJson }

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

Equations

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

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

Equations

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

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

Equations

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

instance Lake.Manifest.instFromJson : Lean.FromJson Manifest

Equations

• Lake.Manifest.instFromJson = { fromJson? := Lake.Manifest.fromJson? }

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

Parse a Manifest from a string.

Equations

• Lake.Manifest.parse data = match Lean.Json.parse data with | Except.ok json => Lean.fromJson? json | Except.error e => throw (toString "invalid JSON: " ++ toString e ++ toString "")

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

Parse a manifest file.

Equations

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

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.

Equations

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

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

Serialize the manifest to a JSON file.

Equations

• self.save manifestFile = IO.FS.writeFile manifestFile (self.toJson.pretty.push '\n')

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

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

Equations

• Lake.Manifest.saveToFile = Lake.Manifest.save

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

Deserialize package entries from a (partial) JSON manifest.

Equations

• Lake.Manifest.decodeEntries data = do let obj ← Lake.JsonObject.fromJson? data let __do_lift ← Lake.Manifest.getVersion obj Lake.Manifest.getPackages (Lake.StdVer.ofSemVerCore __do_lift) obj

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

Deserialize manifest package entries from a JSON string.

Equations

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

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

Deserialize manifest package entries from a JSON file.

Equations

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

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.

Equations

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

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

Serialize manifest package entries to a JSON file.

Equations

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