From cfc8a2538dbd26b03d3d421a669c4fe3617e7022 Mon Sep 17 00:00:00 2001 From: tydeu Date: Sat, 2 Oct 2021 14:21:45 -0400 Subject: [PATCH] refactor: generalize `buildTop` and `failOnImportCycle` Reason: will be useful for upcoming dependency build fix --- Lake/BuildMonad.lean | 4 ++-- Lake/BuildPackage.lean | 12 ++++++------ Lake/BuildTop.lean | 25 ++++++++++++------------- 3 files changed, 20 insertions(+), 21 deletions(-) diff --git a/Lake/BuildMonad.lean b/Lake/BuildMonad.lean index 2651b13643..7c4226226a 100644 --- a/Lake/BuildMonad.lean +++ b/Lake/BuildMonad.lean @@ -95,11 +95,11 @@ def run (self : BuildM α) : IO PUnit := end BuildM -def failOnImportCycle : Except (List Lean.Name) α → BuildM α +def failOnBuildCycle [ToString k] : Except (List k) α → BuildM α | Except.ok a => a | Except.error cycle => do let cycle := cycle.map (s!" {·}") - let msg := s!"import cycle detected:\n{"\n".intercalate cycle}" + let msg := s!"build cycle detected:\n{"\n".intercalate cycle}" BuildM.logError msg throw <| IO.userError msg diff --git a/Lake/BuildPackage.lean b/Lake/BuildPackage.lean index a0d26ad8ef..f01e88c600 100644 --- a/Lake/BuildPackage.lean +++ b/Lake/BuildPackage.lean @@ -39,16 +39,16 @@ def Package.buildModuleOleanAndCTargetDAG (self : Package) : BuildM (Array ActiveOleanAndCTarget × OleanAndCTargetMap) := do let buildMod : OleanAndCTargetBuild := self.recBuildModuleOleanAndCTargetWithLocalImports moreOleanDirs depTarget - let (resE, map) ← mods.mapM (buildRBTop buildMod) |>.run {} - (← failOnImportCycle resE, map) + let (resE, map) ← mods.mapM (buildRBTop buildMod id) |>.run {} + (← failOnBuildCycle resE, map) def Package.buildModuleOleanTargetDAG (mods : Array Name) (moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x) (self : Package) : BuildM (Array ActiveFileTarget × OleanTargetMap) := do let buildMod : OleanTargetBuild := self.recBuildModuleOleanTargetWithLocalImports moreOleanDirs depTarget - let (resE, map) ← mods.mapM (buildRBTop buildMod) |>.run {} - (← failOnImportCycle resE, map) + let (resE, map) ← mods.mapM (buildRBTop buildMod id) |>.run {} + (← failOnBuildCycle resE, map) def Package.buildOleanAndCTargetDAG (moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x) @@ -65,14 +65,14 @@ def Package.buildModuleOleanAndCTargets (self : Package) : BuildM (Array ActiveOleanAndCTarget) := do let buildMod : OleanAndCTargetBuild := self.recBuildModuleOleanAndCTargetWithLocalImports moreOleanDirs depTarget - failOnImportCycle <| ← mods.mapM (buildRBTop buildMod) |>.run' {} + failOnBuildCycle <| ← mods.mapM (buildRBTop buildMod id) |>.run' {} def Package.buildModuleOleanTargets (mods : Array Name) (moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x) (self : Package) : BuildM (Array ActiveFileTarget) := do let buildMod : OleanTargetBuild := self.recBuildModuleOleanTargetWithLocalImports moreOleanDirs depTarget - failOnImportCycle <| ← mods.mapM (buildRBTop buildMod) |>.run' {} + failOnBuildCycle <| ← mods.mapM (buildRBTop buildMod id) |>.run' {} def Package.buildOleanAndCTargets (moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x) diff --git a/Lake/BuildTop.lean b/Lake/BuildTop.lean index 2d54644cfc..d0b4e025dd 100644 --- a/Lake/BuildTop.lean +++ b/Lake/BuildTop.lean @@ -15,8 +15,8 @@ namespace Lake -- ## Abstractions /-- A recursive object builder. -/ -def RecBuild.{u,v,w} (k : Type u) (o : Type v) (m : Type v → Type w) := - k → (k → m o) → m o +def RecBuild.{u,v,w} (i : Type u) (o : Type v) (m : Type v → Type w) := + i → (i → m o) → m o /-- A monad equipped with a key-object store. -/ class MonadStore (k : Type u) (o : Type v) (m : Type v → Type w) where @@ -32,9 +32,9 @@ instance [Monad m] [MonadStore k o m] : MonadStore k o (ExceptT ε m) where -- ## Algorithm /-- Auxiliary function for `buildTop`. -/ -partial def buildTopCore -{k o} {m} [BEq k] [Inhabited o] [Monad m] [MonadStore k o m] -(parents : List k) (build : RecBuild k o (ExceptT (List k) m)) (key : k) : ExceptT (List k) m o := do +partial def buildTopCore [BEq k] [Inhabited o] [Monad m] [MonadStore k o m] +(parents : List k) (build : RecBuild i o (ExceptT (List k) m)) (keyOf : i → k) (info : i) : ExceptT (List k) m o := do + let key := keyOf info -- detect cyclic builds if parents.contains key then throw <| key :: (parents.partition (· != key)).1 ++ [key] @@ -42,20 +42,19 @@ partial def buildTopCore if let some output ← fetch? key then return output -- build the key recursively - let output ← build key (buildTopCore (key :: parents) build) + let output ← build info <| buildTopCore (key :: parents) build keyOf -- save the output (to prevent repeated builds of the same key) store key output return output /-- Recursively fills a `MonadStore` of key-object pairs by - fetching objects topologically (i.e., via a depth-first search with memoization). + building objects topologically (i.e., via a depth-first search with memoization). Called a suspending scheduler in "Build systems à la carte". -/ -def buildTop -{k o} {m} [BEq k] [Inhabited o] [Monad m] [MonadStore k o m] -(build : RecBuild k o (ExceptT (List k) m)) (key : k) : ExceptT (List k) m o := - buildTopCore [] build key +def buildTop [BEq k] [Inhabited o] [Monad m] [MonadStore k o m] +(build : RecBuild i o (ExceptT (List k) m)) (keyOf : i → k) (info : i) : ExceptT (List k) m o := + buildTopCore [] build keyOf info -------------------------------------------------------------------------------- -- # RBMap Version @@ -88,5 +87,5 @@ abbrev RBTopT.{u,v} (k : Type u) (o : Type u) (cmp) (m : Type u → Type v) := /-- The `RBMap` version of `buildTop`. -/ def buildRBTop {k o} {cmp} {m} [BEq k] [Inhabited o] [Monad m] -(build : RecBuild k o (RBTopT k o cmp m)) (key : k) : RBTopT k o cmp m o := - buildTop build key +(build : RecBuild i o (RBTopT k o cmp m)) (keyOf : i → k) (info : i) : RBTopT k o cmp m o := + buildTop build keyOf info