Documentation

Lake.Load.Manifest

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 :

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, patch := 0, specialDescr := "" }

inductive Lake.PackageEntryV6 :

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

Instances For

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 :

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.

Instances For

Lake.instInhabitedPackageEntrySrc

instance Lake.instInhabitedPackageEntrySrc :

Inhabited PackageEntrySrc

Equations

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

structure Lake.PackageEntry :

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

Instances For

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) :

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) :

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) :

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

def Lake.PackageEntry.ofV6 :

PackageEntryV6 → PackageEntry

Equations

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

structure Lake.Manifest :

Manifest data structure that is serialized to the file.

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

Instances For

def Lake.Manifest.addPackage (entry : PackageEntry) (self : 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) :

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) :

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) :

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) :

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) :

Serialize manifest package entries to a JSON file.

Equations

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