From db304448de8decdd5dad112b9e32a795b2594713 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 28 May 2021 15:13:52 +0200 Subject: [PATCH] fix: leanpkg: rebuild if dependencies or `leanpkg.toml` (e.g. `lean_version`) changed --- src/Leanpkg.lean | 34 ++++++++++++++++++++-------------- src/Leanpkg/Build.lean | 29 +++++++++++++++-------------- 2 files changed, 35 insertions(+), 28 deletions(-) diff --git a/src/Leanpkg.lean b/src/Leanpkg.lean index 2d9ba30933..5024d7c025 100644 --- a/src/Leanpkg.lean +++ b/src/Leanpkg.lean @@ -50,15 +50,24 @@ partial def withLockFile (x : IO α) : IO α := do acquire (firstTime := false) | e => throw e +def getRootPart (pkg : FilePath := ".") : IO Lean.Name := do + let entries ← pkg.readDir + match entries.filter (FilePath.extension ·.fileName == "lean") with + | #[rootFile] => FilePath.withExtension rootFile.fileName "" |>.toString + | #[] => throw <| IO.userError s!"no '.lean' file found in {← IO.realPath "."}" + | _ => throw <| IO.userError s!"{← IO.realPath "."} must contain a unique '.lean' file as the package root" + structure Configuration := leanPath : String leanSrcPath : String + moreDeps : List FilePath def configure : IO Configuration := do let d ← readManifest IO.eprintln $ "configuring " ++ d.name ++ " " ++ d.version let assg ← solveDeps d let paths ← constructPath assg + let mut moreDeps := [leanpkgTomlFn] for path in paths do unless path == FilePath.mk "." / "." do -- build recursively @@ -68,28 +77,23 @@ def configure : IO Configuration := do cwd := path args := #["build"] } + moreDeps := (path / Build.buildPath / (← getRootPart path).toString |>.withExtension "olean") :: moreDeps return { leanPath := SearchPath.toString <| paths.map (· / Build.buildPath) leanSrcPath := SearchPath.toString paths + moreDeps } -def execMake (makeArgs leanArgs : List String) (leanPath : String) : IO Unit := withLockFile do +def execMake (makeArgs : List String) (cfg : Build.Config) : IO Unit := withLockFile do let manifest ← readManifest - let leanArgs := (match manifest.timeout with | some t => ["-T", toString t] | none => []) ++ leanArgs + let leanArgs := (match manifest.timeout with | some t => ["-T", toString t] | none => []) ++ cfg.leanArgs let mut spawnArgs := { cmd := "sh" cwd := manifest.effectivePath - args := #["-c", s!"\"{← IO.appDir}/leanmake\" LEAN_OPTS=\"{" ".intercalate leanArgs}\" LEAN_PATH=\"{leanPath}\" {" ".intercalate makeArgs} >&2"] + args := #["-c", s!"\"{← IO.appDir}/leanmake\" PKG={cfg.pkg} LEAN_OPTS=\"{" ".intercalate leanArgs}\" LEAN_PATH=\"{cfg.leanPath}\" {" ".intercalate makeArgs} MORE_DEPS+=\"{" ".intercalate (cfg.moreDeps.map toString)}\" >&2"] } execCmd spawnArgs -def getRootPart : IO Lean.Name := do - let entries ← FilePath.readDir "." - match entries.filter (FilePath.extension ·.fileName == "lean") with - | #[rootFile] => FilePath.withExtension rootFile.fileName "" |>.toString - | #[] => throw <| IO.userError s!"no '.lean' file found in {← IO.realPath "."}" - | _ => throw <| IO.userError s!"{← IO.realPath "."} must contain a unique '.lean' file as the package root" - def buildImports (imports : List String) (leanArgs : List String) : IO Unit := do unless ← leanpkgTomlFn.pathExists do return @@ -99,21 +103,23 @@ def buildImports (imports : List String) (leanArgs : List String) : IO Unit := d let root ← getRootPart let localImports := imports.filter (·.getRoot == root) if localImports != [] then + let buildCfg : Build.Config := { 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 - execMake oleans leanArgs cfg.leanPath + execMake oleans buildCfg else - Build.buildModules root localImports leanArgs cfg.leanPath + Build.buildModules buildCfg localImports IO.println cfg.leanPath IO.println cfg.leanSrcPath def build (makeArgs leanArgs : List String) : IO Unit := do let cfg ← configure let root ← getRootPart + let buildCfg : Build.Config := { pkg := root, leanArgs, leanPath := cfg.leanPath, moreDeps := cfg.moreDeps } if makeArgs != [] || (← FilePath.pathExists "Makefile") then - execMake (s!"PKG={root}" :: makeArgs) leanArgs cfg.leanPath + execMake leanArgs buildCfg else - Build.buildModules root [root] leanArgs cfg.leanPath + Build.buildModules buildCfg [root] def initGitignoreContents := "/build diff --git a/src/Leanpkg/Build.lean b/src/Leanpkg/Build.lean index 9e2bfe14ad..423f89023b 100644 --- a/src/Leanpkg/Build.lean +++ b/src/Leanpkg/Build.lean @@ -15,11 +15,16 @@ namespace Leanpkg.Build def buildPath : FilePath := "build" def tempBuildPath := buildPath / "temp" -structure Context where +structure Config where pkg : Name leanArgs : List String leanPath : String - parents : List Name := [] + -- 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 structure Result where maxMTime : IO.FS.SystemTime @@ -48,15 +53,10 @@ partial def buildModule (mod : Name) : BuildM Result := do -- recursively build dependencies and calculate transitive `maxMTime` let (imports, _, _) ← Elab.parseImports (← IO.FS.readFile leanFile) leanFile.toString - let mut deps := #[] - let mut maxMTime := leanMData.modified - for i in imports do - if i.module.getRoot == ctx.pkg then - let dep ← withReader (fun ctx => { ctx with parents := mod :: ctx.parents }) do - buildModule i.module - if dep.maxMTime > maxMTime then - maxMTime := dep.maxMTime - deps := deps.push dep + 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 buildPath mod "olean" @@ -69,7 +69,7 @@ partial def buildModule (mod : Name) : BuildM Result := do | IO.Error.noFileOrDirectory .. => pure () | e => throw e - let task ← IO.mapTasks (tasks := deps.map (·.task) |>.toList) fun rs => do + 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 @@ -91,8 +91,9 @@ partial def buildModule (mod : Name) : BuildM Result := do modify fun st => { st with modTasks := st.modTasks.insert mod r } return r -def buildModules (pkg : Name) (mods : List Name) (leanArgs : List String) (leanPath : String) : IO Unit := do - let rs ← mods.mapM buildModule |>.run { pkg, leanArgs, leanPath } |>.run' {} +def buildModules (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 } |>.run' {} for r in rs do if let Except.error _ ← IO.wait r.task then -- actual error has already been printed above