feat: lake: builtin facet memoize toggle (#7738)

This PR makes memoization of built-in facets toggleable through a
`memoize` option on the facet configuration. Built-in facets which are
essentially aliases (e.g., `default`, `o`) have had memoization
disabled.

Author: tydeu

src/lake/Lake/Build/Executable.lean

@@ -50,7 +50,7 @@ def LeanExe.recBuildDefault (lib : LeanExe) : FetchM (Job FilePath) :=
 
 /-- The facet configuration for the builtin `ExternLib.dynlibFacet`. -/
 def LeanExe.defaultFacetConfig : LeanExeFacetConfig defaultFacet :=
-  mkFacetJobConfig recBuildDefault
+  mkFacetJobConfig recBuildDefault (memoize := false)
 
 /--
 A name-configuration map for the initial set of

src/lake/Lake/Build/ExternLib.lean

@@ -81,7 +81,7 @@ def ExternLib.recBuildDefault (lib : ExternLib) : FetchM (Job FilePath) :=
 
 /-- The facet configuration for the builtin `ExternLib.dynlibFacet`. -/
 def ExternLib.defaultFacetConfig : ExternLibFacetConfig defaultFacet :=
-  mkFacetJobConfig recBuildDefault
+  mkFacetJobConfig recBuildDefault (memoize := false)
 
 /--
 A name-configuration map for the initial set of

src/lake/Lake/Build/Index.lean

@@ -22,30 +22,37 @@ open System (FilePath)
 namespace Lake
 
 /-- Recursive build function for anything in the Lake build index. -/
-def recBuildWithIndex (info : BuildInfo) : FetchM (Job (BuildData info.key)) :=
+def recBuildWithIndex (info : BuildInfo) : FetchM (Job (BuildData info.key)) := do
   match info with
-  | .target pkg target => do
+  | .target pkg target =>
     if let some decl := pkg.findTargetDecl? target then
       if h : decl.kind.isAnonymous then
-        (decl.targetConfig h).fetchFn pkg
+        let key := BuildKey.packageTarget pkg.name target
+        fetchOrCreate key do (decl.targetConfig h).fetchFn pkg
       else
         let kind := ⟨decl.kind, by simp [decl.target_eq_type h]⟩
         let job := Job.pure (kind := kind) <| decl.mkConfigTarget pkg
         return cast (by simp [decl.data_eq_target h]) job
     else
       error s!"invalid target '{info}': target not found in package"
-  | .facet _ kind data facet => do
+  | .facet target kind data facet =>
     if let some config := (← getWorkspace).findFacetConfig? facet then
       if h : config.kind = kind then
-        config.fetchFn <| cast (by simp [h]) data
+        let recFetch := config.fetchFn <| cast (by simp [h]) data
+        if config.memoize then
+          let key := BuildKey.facet target facet
+          fetchOrCreate key recFetch
+        else
+          recFetch
       else
-        error s!"invalid target '{info}': target is of kind '{kind}', but facet expects '{config.kind}'"
+        error s!"invalid target '{info}': \
+          input target is of kind '{kind}', but facet expects '{config.kind}'"
     else
       error s!"invalid target '{info}': unknown facet '{facet}'"
 
 /-- Recursive build function with memoization. -/
 def recFetchWithIndex : (info : BuildInfo) → RecBuildM (Job (BuildData info.key)) :=
- inline <| recFetchMemoize (β := (Job <| BuildData ·)) BuildInfo.key recBuildWithIndex
+ inline <| recFetchAcyclic (β := (Job <| BuildData ·.key)) BuildInfo.key recBuildWithIndex
 
 /--
 Run a recursive Lake build using the Lake build index

src/lake/Lake/Build/Module.lean

@@ -291,7 +291,7 @@ def Module.recBuildLean (mod : Module) : FetchM (Job Unit) := do
 
 /-- The `ModuleFacetConfig` for the builtin `leanArtsFacet`. -/
 def Module.leanArtsFacetConfig : ModuleFacetConfig leanArtsFacet :=
-  mkFacetJobConfig (·.recBuildLean)
+  mkFacetJobConfig recBuildLean
 
 /-- The `ModuleFacetConfig` for the builtin `oleanFacet`. -/
 def Module.oleanFacetConfig : ModuleFacetConfig oleanFacet :=
@@ -377,11 +377,11 @@ def Module.recBuildLeanCToONoExport (self : Module) : FetchM (Job FilePath) := d
 
 /-- The `ModuleFacetConfig` for the builtin `coNoExportFacet`. -/
 def Module.coNoExportFacetConfig : ModuleFacetConfig coNoExportFacet :=
-  mkFacetJobConfig Module.recBuildLeanCToONoExport
+  mkFacetJobConfig recBuildLeanCToONoExport
 
 /-- The `ModuleFacetConfig` for the builtin `coFacet`. -/
 def Module.coFacetConfig : ModuleFacetConfig coFacet :=
-  mkFacetJobConfig fun mod =>
+  mkFacetJobConfig (memoize := false) fun mod =>
     if Platform.isWindows then mod.coNoExport.fetch else mod.coExport.fetch
 
 /-- Recursively build the module's object file from its bitcode file produced by `lean`. -/
@@ -392,25 +392,25 @@ def Module.recBuildLeanBcToO (self : Module) : FetchM (Job FilePath) := do
 
 /-- The `ModuleFacetConfig` for the builtin `bcoFacet`. -/
 def Module.bcoFacetConfig : ModuleFacetConfig bcoFacet :=
-  mkFacetJobConfig Module.recBuildLeanBcToO
+  mkFacetJobConfig recBuildLeanBcToO
 
 /-- The `ModuleFacetConfig` for the builtin `oExportFacet`. -/
 def Module.oExportFacetConfig : ModuleFacetConfig oExportFacet :=
-  mkFacetJobConfig fun mod =>
+  mkFacetJobConfig (memoize := false) fun mod =>
     match mod.backend with
     | .default | .c => mod.coExport.fetch
     | .llvm => mod.bco.fetch
 
 /-- The `ModuleFacetConfig` for the builtin `oNoExportFacet`. -/
 def Module.oNoExportFacetConfig : ModuleFacetConfig oNoExportFacet :=
-  mkFacetJobConfig fun mod =>
+  mkFacetJobConfig (memoize := false) fun mod =>
     match mod.backend with
     | .default | .c => mod.coNoExport.fetch
     | .llvm => error "the LLVM backend only supports exporting Lean symbols"
 
 /-- The `ModuleFacetConfig` for the builtin `oFacet`. -/
 def Module.oFacetConfig : ModuleFacetConfig oFacet :=
-  mkFacetJobConfig fun mod =>
+  mkFacetJobConfig (memoize := false) fun mod =>
     match mod.backend with
     | .default | .c => mod.co.fetch
     | .llvm => mod.bco.fetch
@@ -444,7 +444,7 @@ def Module.recBuildDynlib (mod : Module) : FetchM (Job Dynlib) :=
 
 /-- The `ModuleFacetConfig` for the builtin `dynlibFacet`. -/
 def Module.dynlibFacetConfig : ModuleFacetConfig dynlibFacet :=
-  mkFacetJobConfig Module.recBuildDynlib
+  mkFacetJobConfig recBuildDynlib
 
 /--
 A name-configuration map for the initial set of

src/lake/Lake/Config/FacetConfig.lean

@@ -22,6 +22,8 @@ structure FacetConfig (name : Name) : Type where
   buildable : Bool := true
   /-- Format this facet's output (e.g., for `lake query`). -/
   format : OutFormat → FacetOut name → String
+  /-- Whether the fetch of this facet should be cached in the Lake build store. -/
+  memoize : Bool := true
   deriving Inhabited
 
 protected abbrev FacetConfig.name (_ : FacetConfig name) := name
@@ -54,9 +56,10 @@ def FacetConfig.toKind? (kind : Name) (self : FacetConfig name) : Option (KFacet
   [outKind : OptDataKind β]
   [i : FamilyOut DataType kind α]
   [o : FamilyOut FacetOut facet β]
-  (build : α → FetchM (Job β)) (buildable := true)
+  (build : α → FetchM (Job β))
+  (buildable := true) (memoize := true)
 : KFacetConfig kind facet where
-  buildable
+  buildable; memoize
   outKind := o.fam_eq ▸ outKind
   fetchFn := i.fam_eq ▸ o.fam_eq ▸ build
   format := o.fam_eq ▸ formatQuery