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

refactor: generalize buildTop and failOnImportCycle

Browse source 
Reason: will be useful for upcoming dependency build fix
This commit is contained in:
tydeu 2021-10-02 14:21:45 -04:00
parent 83ccf8a15d
commit cfc8a2538d
3 changed files with 20 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
Lake/BuildMonad.lean
View file

@ -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

12
Lake/BuildPackage.lean
View file

@ -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)

25
Lake/BuildTop.lean
View file

@ -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