max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: lake: add name to manifest

Browse source
This commit is contained in:
tydeu 2023-09-20 12:15:33 -04:00 • committed by Mac Malone
parent dc60150b5a
commit ec217caf22
2 changed files with 12 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/lake/Lake/Load/Main.lean
View file

@ -87,7 +87,7 @@ def buildUpdatedManifest (ws : Workspace)
return {pkg with opaqueDeps := ← deps.mapM (.mk <$> resolve ·)}
match res with
| (.ok root, deps) =>
let manifest : Manifest := {packagesDir? := ws.relPkgsDir}
let manifest : Manifest := {name? := ws.root.name, packagesDir? := ws.relPkgsDir}
let manifest := deps.foldl (fun m d => m.addPackage d.manifestEntry) manifest
return ({ws with root}, manifest)
| (.error cycle, _) =>

19
src/lake/Lake/Load/Manifest.lean
View file

@ -23,7 +23,7 @@ instance [FromJson α] : FromJson (NameMap α) where
return m.insert k (← fromJson? v)
/-- Current version of the manifest format. -/
def Manifest.version : Nat := 5
def Manifest.version : Nat := 6
/-- An entry for a package stored in the manifest. -/
inductive PackageEntry
@ -60,6 +60,7 @@ end PackageEntry
/-- Manifest data structure that is serialized to the file. -/
structure Manifest where
name? : Option Name := none
packagesDir? : Option FilePath := none
packages : Array PackageEntry := #[]
@ -77,10 +78,11 @@ instance : ForIn m Manifest PackageEntry where
forIn self init f := self.packages.forIn init f
protected def toJson (self : Manifest) : Json :=
Json.mkObj [
("version", version),
("packagesDir", toJson self.packagesDir?),
("packages", toJson self.packages)
Json.mkObj <| .join [
[("version", version)],
Json.opt "name" self.name?,
[("packagesDir", toJson self.packagesDir?)],
[("packages", toJson self.packages)]
]
instance : ToJson Manifest := ⟨Manifest.toJson⟩
@ -90,16 +92,17 @@ protected def fromJson? (json : Json) : Except String Manifest := do
let .ok ver := ver.getNat? | throw s!"unknown manifest version `{ver}`"
if ver < 5 then
throw s!"incompatible manifest version `{ver}`"
else if ver = 5 then
else if ver ≤ 6 then
let name? ← json.getObjValAs? _ "name"
let packagesDir? ← do
match json.getObjVal? "packagesDir" with
| .ok path => fromJson? path
| .error _ => pure none
let packages : Array PackageEntry ← fromJson? (← json.getObjVal? "packages")
return {packagesDir?, packages}
return {name?, packagesDir?, packages}
else
throw <|
s!"manifest version `{ver}` is higher than this Lake's '{Manifest.version}';" ++
s!"manifest version `{ver}` is higher than this Lake's '{Manifest.version}'; " ++
"you may need to update your `lean-toolchain`"
instance : FromJson Manifest := ⟨Manifest.fromJson?⟩