From 44b9ad2a30942c714fc63fc0aad16e497bf3bd38 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Sat, 29 May 2021 12:38:29 -0400 Subject: [PATCH] Assorted code cleanup and reogranization --- Leanpkg2/Build.lean | 108 +++++++++++++++++++++++++++++++++---- Leanpkg2/BuildConfig.lean | 24 +++++++++ Leanpkg2/BuildCore.lean | 106 ------------------------------------ Leanpkg2/Cli.lean | 4 +- Leanpkg2/Configure.lean | 12 ++--- Leanpkg2/Init.lean | 4 +- Leanpkg2/Make.lean | 6 +-- Leanpkg2/Manifest.lean | 64 +--------------------- Leanpkg2/Resolve.lean | 8 +-- Leanpkg2/TomlManifest.lean | 77 ++++++++++++++++++++++++++ 10 files changed, 218 insertions(+), 195 deletions(-) create mode 100644 Leanpkg2/BuildConfig.lean delete mode 100644 Leanpkg2/BuildCore.lean create mode 100644 Leanpkg2/TomlManifest.lean diff --git a/Leanpkg2/Build.lean b/Leanpkg2/Build.lean index 31c04627fe..7cc2946c4d 100644 --- a/Leanpkg2/Build.lean +++ b/Leanpkg2/Build.lean @@ -3,35 +3,125 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone -/ +import Lean.Data.Name +import Lean.Elab.Import import Leanpkg2.Resolve -import Leanpkg2.BuildCore +import Leanpkg2.Manifest +import Leanpkg2.BuildConfig import Leanpkg2.Configure import Leanpkg2.Make +import Leanpkg2.Proc -open System +open Lean System namespace Leanpkg2 -def buildImports (manifest : Manifest) (imports : List String) (leanArgs : List String) : IO Unit := do - let cfg ← configure manifest +structure BuildContext extends BuildConfig where + parents : List Name := [] + moreDepsMTime : IO.FS.SystemTime + manifest : Manifest + +deriving instance Inhabited for IO.FS.SystemTime +deriving instance Inhabited for Task + +structure Result where + maxMTime : IO.FS.SystemTime + task : Task (Except IO.Error Unit) + deriving Inhabited + +structure State where + modTasks : NameMap Result := ∅ + +abbrev BuildM := ReaderT BuildContext <| StateT State IO + +partial def buildModule (mod : Name) : BuildM Result := do + let ctx ← read + if ctx.parents.contains mod then + -- cyclic import + let cycle := ctx.parents.dropWhile (· != mod) ++ [mod] + let cycle := cycle.reverse.map (s!" {·}") + throw <| IO.userError s!"import cycle detected:\n{"\n".intercalate cycle}" + + if let some r := (← get).modTasks.find? mod then + -- already visited + return r + + let srcPath := ctx.manifest.effectivePath + let leanFile := modToFilePath srcPath mod "lean" + let leanMData ← leanFile.metadata + + -- recursively build dependencies and calculate transitive `maxMTime` + let (imports, _, _) ← Elab.parseImports (← IO.FS.readFile leanFile) leanFile.toString + let localImports := imports.filter (·.module.getRoot == ctx.pkg) + let deps ← localImports.mapM (buildModule ·.module) + let depMTimes ← deps.mapM (·.maxMTime) + let maxMTime := List.maximum? (leanMData.modified :: ctx.moreDepsMTime :: depMTimes) |>.get! + + -- check whether we have an up-to-date .olean + let oleanFile := modToFilePath (srcPath / buildPath) mod "olean" + try + if (← oleanFile.metadata).modified >= maxMTime then + let r := { maxMTime, task := Task.pure (Except.ok ()) } + modify fun st => { st with modTasks := st.modTasks.insert mod r } + return r + catch + | IO.Error.noFileOrDirectory .. => pure () + | e => throw e + + let task ← IO.mapTasks (tasks := deps.map (·.task)) fun rs => do + if let some e := rs.findSome? (fun | Except.error e => some e | Except.ok _ => none) then + -- propagate failure + throw e + try + let cFile := modToFilePath (srcPath / tempBuildPath) mod "c" + IO.createDirAll oleanFile.parent.get! + IO.createDirAll cFile.parent.get! + execCmd { + cmd := (← IO.appDir) / "lean" |>.withExtension FilePath.exeExtension |>.toString + args := ctx.leanArgs.toArray ++ #["-o", oleanFile.toString, "-c", cFile.toString, leanFile.toString] + env := #[("LEAN_PATH", ctx.leanPath)] + } + catch e => + -- print errors early + IO.eprintln e + throw e + + let r := { maxMTime, task := task } + modify fun st => { st with modTasks := st.modTasks.insert mod r } + return r + +def buildModules (manifest : Manifest) (cfg : BuildConfig) (mods : List Name) : IO Unit := do + let moreDepsMTime := (← cfg.moreDeps.mapM (·.metadata)).map (·.modified) |>.maximum? |>.getD ⟨0, 0⟩ + let rs ← mods.mapM buildModule |>.run { toBuildConfig := cfg, moreDepsMTime, manifest } |>.run' {} + for r in rs do + if let Except.error _ ← IO.wait r.task then + -- actual error has already been printed above + throw <| IO.userError "Build failed." + +def buildImports (manifest : Manifest) (cfg : Configuration) (imports leanArgs : List String := []) : IO Unit := do let imports := imports.map (·.toName) let root ← getRootPart <| manifest.effectivePath let localImports := imports.filter (·.getRoot == root) if localImports != [] then - let buildCfg : Build.Config := { pkg := root, leanArgs, leanPath := cfg.leanPath, moreDeps := cfg.moreDeps } + let buildCfg : BuildConfig := { pkg := root, leanArgs, leanPath := cfg.leanPath, moreDeps := cfg.moreDeps } if ← FilePath.pathExists "Makefile" then - let oleans := localImports.map fun i => Lean.modToFilePath "build" i "olean" |>.toString + let oleans := localImports.map fun i => + Lean.modToFilePath (manifest.effectivePath / buildPath) i "olean" |>.toString execMake manifest oleans buildCfg else - Build.buildModules manifest buildCfg localImports + buildModules manifest buildCfg localImports + +def printPaths (manifest : Manifest) (imports leanArgs : List String := []) : IO Unit := do + let cfg ← configure manifest + buildImports manifest cfg imports leanArgs IO.println cfg.leanPath IO.println cfg.leanSrcPath def build (manifest : Manifest) (makeArgs leanArgs : List String := []) : IO Unit := do let cfg ← configure manifest let root ← getRootPart <| manifest.effectivePath - let buildCfg : Build.Config := { pkg := root, leanArgs, leanPath := cfg.leanPath, moreDeps := cfg.moreDeps } + let buildCfg : BuildConfig := { pkg := root, leanArgs, leanPath := cfg.leanPath, moreDeps := cfg.moreDeps } if makeArgs != [] || (← FilePath.pathExists "Makefile") then execMake manifest makeArgs buildCfg else - Build.buildModules manifest buildCfg [root] + buildModules manifest buildCfg [root] diff --git a/Leanpkg2/BuildConfig.lean b/Leanpkg2/BuildConfig.lean new file mode 100644 index 0000000000..390de4d48a --- /dev/null +++ b/Leanpkg2/BuildConfig.lean @@ -0,0 +1,24 @@ +/- +Copyright (c) 2021 Sebastian Ullrich. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sebastian Ullrich +-/ +import Lean.Data.Name +import Lean.Elab.Import +import Leanpkg2.Manifest +import Leanpkg2.Proc + +open Lean +open System + +namespace Leanpkg2 + +def buildPath : FilePath := "build" +def tempBuildPath := buildPath / "temp" + +structure BuildConfig where + pkg : Name + leanArgs : List String + leanPath : String + -- things like `leanpkg.toml` and olean roots of dependencies that should also trigger rebuilds + moreDeps : List FilePath diff --git a/Leanpkg2/BuildCore.lean b/Leanpkg2/BuildCore.lean deleted file mode 100644 index 622d27773d..0000000000 --- a/Leanpkg2/BuildCore.lean +++ /dev/null @@ -1,106 +0,0 @@ -/- -Copyright (c) 2021 Sebastian Ullrich. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Sebastian Ullrich --/ -import Lean.Data.Name -import Lean.Elab.Import -import Leanpkg2.Manifest -import Leanpkg2.Proc - -open Lean -open System - -namespace Leanpkg2.Build - -def buildPath : FilePath := "build" -def tempBuildPath := buildPath / "temp" - -structure Config where - pkg : Name - leanArgs : List String - leanPath : String - -- things like `leanpkg.toml` and olean roots of dependencies that should also trigger rebuilds - moreDeps : List FilePath - -structure Context extends Config where - parents : List Name := [] - moreDepsMTime : IO.FS.SystemTime - manifest : Manifest - -deriving instance Inhabited for IO.FS.SystemTime -deriving instance Inhabited for Task - -structure Result where - maxMTime : IO.FS.SystemTime - task : Task (Except IO.Error Unit) - deriving Inhabited - -structure State where - modTasks : NameMap Result := ∅ - -abbrev BuildM := ReaderT Context <| StateT State IO - -partial def buildModule (mod : Name) : BuildM Result := do - let ctx ← read - if ctx.parents.contains mod then - -- cyclic import - let cycle := ctx.parents.dropWhile (· != mod) ++ [mod] - let cycle := cycle.reverse.map (s!" {·}") - throw <| IO.userError s!"import cycle detected:\n{"\n".intercalate cycle}" - - if let some r := (← get).modTasks.find? mod then - -- already visited - return r - - let srcPath := ctx.manifest.effectivePath - let leanFile := modToFilePath srcPath mod "lean" - let leanMData ← leanFile.metadata - - -- recursively build dependencies and calculate transitive `maxMTime` - let (imports, _, _) ← Elab.parseImports (← IO.FS.readFile leanFile) leanFile.toString - let localImports := imports.filter (·.module.getRoot == ctx.pkg) - let deps ← localImports.mapM (buildModule ·.module) - let depMTimes ← deps.mapM (·.maxMTime) - let maxMTime := List.maximum? (leanMData.modified :: ctx.moreDepsMTime :: depMTimes) |>.get! - - -- check whether we have an up-to-date .olean - let oleanFile := modToFilePath (srcPath / buildPath) mod "olean" - try - if (← oleanFile.metadata).modified >= maxMTime then - let r := { maxMTime, task := Task.pure (Except.ok ()) } - modify fun st => { st with modTasks := st.modTasks.insert mod r } - return r - catch - | IO.Error.noFileOrDirectory .. => pure () - | e => throw e - - let task ← IO.mapTasks (tasks := deps.map (·.task)) fun rs => do - if let some e := rs.findSome? (fun | Except.error e => some e | Except.ok _ => none) then - -- propagate failure - throw e - try - let cFile := modToFilePath (srcPath / tempBuildPath) mod "c" - IO.createDirAll oleanFile.parent.get! - IO.createDirAll cFile.parent.get! - execCmd { - cmd := (← IO.appDir) / "lean" |>.withExtension FilePath.exeExtension |>.toString - args := ctx.leanArgs.toArray ++ #["-o", oleanFile.toString, "-c", cFile.toString, leanFile.toString] - env := #[("LEAN_PATH", ctx.leanPath)] - } - catch e => - -- print errors early - IO.eprintln e - throw e - - let r := { maxMTime, task := task } - modify fun st => { st with modTasks := st.modTasks.insert mod r } - return r - -def buildModules (manifest : Manifest) (cfg : Config) (mods : List Name) : IO Unit := do - let moreDepsMTime := (← cfg.moreDeps.mapM (·.metadata)).map (·.modified) |>.maximum? |>.getD ⟨0, 0⟩ - let rs ← mods.mapM buildModule |>.run { toConfig := cfg, moreDepsMTime, manifest } |>.run' {} - for r in rs do - if let Except.error _ ← IO.wait r.task then - -- actual error has already been printed above - throw <| IO.userError "Build failed." diff --git a/Leanpkg2/Cli.lean b/Leanpkg2/Cli.lean index 9ddd491486..6f6014aa25 100644 --- a/Leanpkg2/Cli.lean +++ b/Leanpkg2/Cli.lean @@ -7,7 +7,7 @@ import Leanpkg2.Init import Leanpkg2.Configure import Leanpkg2.Make import Leanpkg2.Build -import Leanpkg2.Manifest +import Leanpkg2.TomlManifest namespace Leanpkg2 @@ -66,7 +66,7 @@ directory." def cli : (cmd : String) → (leanpkgArgs leanArgs : List String) → IO Unit | "init", [name], [] => init name | "configure", [], [] => discard do configure (← readManifest) -| "print-paths", leanpkgArgs, leanArgs => do buildImports (← readManifest) leanpkgArgs leanArgs +| "print-paths", imports, leanArgs => do printPaths (← readManifest) imports leanArgs | "build", makeArgs, leanArgs => do build (← readManifest) makeArgs leanArgs | "help", ["init"], [] => IO.println helpInit | "help", ["configure"], [] => IO.println helpConfigure diff --git a/Leanpkg2/Configure.lean b/Leanpkg2/Configure.lean index 397b5cc5be..d8e611e551 100644 --- a/Leanpkg2/Configure.lean +++ b/Leanpkg2/Configure.lean @@ -3,7 +3,7 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone -/ -import Leanpkg2.BuildCore +import Leanpkg2.BuildConfig import Leanpkg2.Resolve open System @@ -27,19 +27,19 @@ def configure (manifest : Manifest) : IO Configuration := do "configuring " ++ manifest.name ++ " " ++ manifest.version let paths ← solveDeps manifest let mut moreDeps := [] - for (pkgpath, srcpath) in paths do - unless pkgpath == "." do + for (pkgPath, srcPath) in paths do + unless pkgPath == "." do -- build recursively -- TODO: share build of common dependencies execCmd { cmd := (← IO.appPath).toString - cwd := pkgpath + cwd := pkgPath args := #["build"] } - let pkgRoot := srcpath / Build.buildPath / (← getRootPart srcpath).toString + let pkgRoot := srcPath / buildPath / (← getRootPart srcPath).toString moreDeps := pkgRoot.withExtension "olean" :: moreDeps return { - leanPath := SearchPath.toString <| paths.map (·.2 / Build.buildPath) + leanPath := SearchPath.toString <| paths.map (·.2 / buildPath) leanSrcPath := SearchPath.toString <| paths.map (·.2) moreDeps } diff --git a/Leanpkg2/Init.lean b/Leanpkg2/Init.lean index 41c772a120..bf26c46b1e 100644 --- a/Leanpkg2/Init.lean +++ b/Leanpkg2/Init.lean @@ -5,7 +5,7 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone -/ import Leanpkg2.Git import Leanpkg2.Proc -import Leanpkg2.Manifest +import Leanpkg2.TomlManifest namespace Leanpkg2 @@ -26,7 +26,7 @@ lean_version = \"{leanVersionString}\" " def initPkg (pkgName : String) (fromNew : Bool) : IO Unit := do - IO.FS.writeFile leanpkgTomlFn (leanpkgFileContents pkgName) + IO.FS.writeFile leanpkgToml (leanpkgFileContents pkgName) IO.FS.writeFile ⟨s!"{pkgName.capitalize}.lean"⟩ mainFileContents let h ← IO.FS.Handle.mk ⟨".gitignore"⟩ IO.FS.Mode.append (bin := false) h.putStr initGitignoreContents diff --git a/Leanpkg2/Make.lean b/Leanpkg2/Make.lean index aceda30ccb..a83aba726e 100644 --- a/Leanpkg2/Make.lean +++ b/Leanpkg2/Make.lean @@ -4,13 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone -/ import Leanpkg2.Manifest -import Leanpkg2.BuildCore +import Leanpkg2.BuildConfig open System namespace Leanpkg2 -def lockFileName : System.FilePath := ⟨".leanpkg-lock"⟩ +def lockFileName : System.FilePath := ".leanpkg-lock" partial def withLockFile (x : IO α) : IO α := do acquire @@ -39,7 +39,7 @@ partial def withLockFile (x : IO α) : IO α := do acquire (firstTime := false) | e => throw e -def execMake (manifest : Manifest) (makeArgs : List String) (cfg : Build.Config) : IO Unit := withLockFile do +def execMake (manifest : Manifest) (makeArgs : List String) (cfg : BuildConfig) : IO Unit := withLockFile do let timeoutArgs := match manifest.timeout with | some t => ["-T", toString t] diff --git a/Leanpkg2/Manifest.lean b/Leanpkg2/Manifest.lean index d052ff79b3..6353d3dff5 100644 --- a/Leanpkg2/Manifest.lean +++ b/Leanpkg2/Manifest.lean @@ -3,7 +3,6 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone -/ -import Leanpkg2.Toml import Leanpkg2.LeanVersion open System @@ -11,30 +10,9 @@ open System namespace Leanpkg2 inductive Source where - | path (dir : System.FilePath) : Source + | path (dir : FilePath) : Source | git (url rev : String) (branch : Option String) : Source -namespace Source - -def fromToml (v : Toml.Value) : Option Source := - (do let Toml.Value.str dir ← v.lookup "path" | none - path ⟨dir⟩) <|> - (do let Toml.Value.str url ← v.lookup "git" | none - let Toml.Value.str rev ← v.lookup "rev" | none - match v.lookup "branch" with - | none => git url rev none - | some (Toml.Value.str branch) => git url rev (some branch) - | _ => none) - -def toToml : Source → Toml.Value - | path dir => Toml.Value.table [("path", Toml.Value.str dir.toString)] - | git url rev none => - Toml.Value.table [("git", Toml.Value.str url), ("rev", Toml.Value.str rev)] - | git url rev (some branch) => - Toml.Value.table [("git", Toml.Value.str url), ("branch", Toml.Value.str branch), ("rev", Toml.Value.str rev)] - -end Source - structure Dependency where name : String src : Source @@ -52,44 +30,4 @@ namespace Manifest def effectivePath (m : Manifest) : FilePath := m.path.getD ⟨"."⟩ -def fromToml (t : Toml.Value) : Option Manifest := OptionM.run do - let pkg ← t.lookup "package" - let Toml.Value.str n ← pkg.lookup "name" | none - let Toml.Value.str ver ← pkg.lookup "version" | none - let leanVer ← match pkg.lookup "lean_version" with - | some (Toml.Value.str leanVer) => some leanVer - | none => some leanVersionString - | _ => none - let tm ← match pkg.lookup "timeout" with - | some (Toml.Value.nat timeout) => some (some timeout) - | none => some none - | _ => none - let path ← match pkg.lookup "path" with - | some (Toml.Value.str path) => some (some ⟨path⟩) - | none => some none - | _ => none - let Toml.Value.table deps ← t.lookup "dependencies" <|> some (Toml.Value.table []) | none - let deps ← deps.mapM fun ⟨n, src⟩ => do Dependency.mk n (← Source.fromToml src) - return { name := n, version := ver, leanVersion := leanVer, - path := path, dependencies := deps, timeout := tm } - -def fromFile (fn : System.FilePath) : IO Manifest := do - let cnts ← IO.FS.readFile fn - let toml ← Toml.parse cnts - let some manifest ← pure (fromToml toml) - | throw <| IO.userError s!"cannot read manifest from {fn}" - manifest - end Manifest - -def leanpkgTomlFn : System.FilePath := ⟨"leanpkg.toml"⟩ - -def readManifest : IO Manifest := do - let m ← Manifest.fromFile leanpkgTomlFn - if m.leanVersion ≠ leanVersionString then - IO.eprintln $ "\nWARNING: Lean version mismatch: installed version is " ++ leanVersionString - ++ ", but package requires " ++ m.leanVersion ++ "\n" - return m - -def writeManifest (manifest : Lean.Syntax) (fn : FilePath) : IO Unit := do - IO.FS.writeFile fn manifest.reprint.get! diff --git a/Leanpkg2/Resolve.lean b/Leanpkg2/Resolve.lean index 79a6d21cee..5af57d81a4 100644 --- a/Leanpkg2/Resolve.lean +++ b/Leanpkg2/Resolve.lean @@ -3,9 +3,9 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone -/ -import Leanpkg2.Manifest -import Leanpkg2.Proc import Leanpkg2.Git +import Leanpkg2.Proc +import Leanpkg2.TomlManifest open System @@ -65,13 +65,13 @@ def solveDepsCore (relPath : FilePath) (d : Manifest) : (maxDepth : Nat) → Sol deps.forM (materialize relPath) for dep in deps do let p ← resolvedPath dep.name - let d' ← Manifest.fromFile $ p / "leanpkg.toml" + let d' ← Manifest.fromTomlFile <| p / "leanpkg.toml" unless d'.name = dep.name do throw <| IO.userError s!"{d.name} (in {relPath}) depends on {d'.name}, but resolved dependency has name {dep.name} (in {p})" solveDepsCore p d' maxDepth def constructPath (depname : String) (dirname : FilePath) : IO (FilePath × FilePath) := do - let path ← Manifest.effectivePath (← Manifest.fromFile <| dirname / leanpkgTomlFn) + let path ← Manifest.effectivePath (← Manifest.fromTomlFile <| dirname / leanpkgToml) (dirname, dirname / path) def solveDeps (d : Manifest) : IO (List (FilePath × FilePath)) := do diff --git a/Leanpkg2/TomlManifest.lean b/Leanpkg2/TomlManifest.lean new file mode 100644 index 0000000000..43a1965fbe --- /dev/null +++ b/Leanpkg2/TomlManifest.lean @@ -0,0 +1,77 @@ +/- +Copyright (c) 2017 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone +-/ +import Leanpkg2.Toml +import Leanpkg2.LeanVersion +import Leanpkg2.Manifest + +open System + +namespace Leanpkg2 + +namespace Source + +def fromToml (v : Toml.Value) : Option Source := + (do let Toml.Value.str dir ← v.lookup "path" | none + path ⟨dir⟩) <|> + (do let Toml.Value.str url ← v.lookup "git" | none + let Toml.Value.str rev ← v.lookup "rev" | none + match v.lookup "branch" with + | none => git url rev none + | some (Toml.Value.str branch) => git url rev (some branch) + | _ => none) + +def toToml : Source → Toml.Value + | path dir => Toml.Value.table [("path", Toml.Value.str dir.toString)] + | git url rev none => + Toml.Value.table [("git", Toml.Value.str url), ("rev", Toml.Value.str rev)] + | git url rev (some branch) => + Toml.Value.table [("git", Toml.Value.str url), ("branch", Toml.Value.str branch), ("rev", Toml.Value.str rev)] + +end Source + +namespace Manifest + +def fromToml (t : Toml.Value) : Option Manifest := OptionM.run do + let pkg ← t.lookup "package" + let Toml.Value.str n ← pkg.lookup "name" | none + let Toml.Value.str ver ← pkg.lookup "version" | none + let leanVer ← match pkg.lookup "lean_version" with + | some (Toml.Value.str leanVer) => some leanVer + | none => some leanVersionString + | _ => none + let tm ← match pkg.lookup "timeout" with + | some (Toml.Value.nat timeout) => some (some timeout) + | none => some none + | _ => none + let path ← match pkg.lookup "path" with + | some (Toml.Value.str path) => some (some ⟨path⟩) + | none => some none + | _ => none + let Toml.Value.table deps ← t.lookup "dependencies" <|> some (Toml.Value.table []) | none + let deps ← deps.mapM fun ⟨n, src⟩ => do Dependency.mk n (← Source.fromToml src) + return { name := n, version := ver, leanVersion := leanVer, + path := path, dependencies := deps, timeout := tm } + +def fromTomlFile (fn : System.FilePath) : IO Manifest := do + let cnts ← IO.FS.readFile fn + let toml ← Toml.parse cnts + let some manifest ← pure (fromToml toml) + | throw <| IO.userError s!"cannot read manifest from {fn}" + manifest + +end Manifest + +def leanpkgToml : System.FilePath := "leanpkg.toml" + +def readManifest : IO Manifest := do + let m ← Manifest.fromTomlFile leanpkgToml + if m.leanVersion ≠ leanVersionString then + IO.eprintln $ "\nWARNING: Lean version mismatch: installed version is " ++ leanVersionString + ++ ", but package requires " ++ m.leanVersion ++ "\n" + return m + +def writeManifest (manifest : Lean.Syntax) (fn : FilePath) : IO Unit := do + IO.FS.writeFile fn manifest.reprint.get!