fix: leanpkg: rebuild if dependencies or leanpkg.toml (e.g. lean_version) changed

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

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