chore: hash field in Name was dropped

Lake/Build/Data.lean

@@ -21,7 +21,7 @@ for the `lean.imports` facet or an active build target for `lean.c`.
 It is an open type, meaning additional mappings can be add lazily
 as needed (via `module_data`).
 -/
-opaque ModuleData (facet : WfName) : Type
+opaque ModuleData (facet : Name) : Type
 
 /--
 The open type family which maps a package facet's name to it build data
@@ -31,7 +31,7 @@ for the facet `deps`.
 It is an open type, meaning additional mappings can be add lazily
 as needed (via `package_data`).
 -/
-opaque PackageData (facet : WfName) : Type
+opaque PackageData (facet : Name) : Type
 
 /--
 The open type family which maps a (builtin) Lake target's (e.g., `extern_lib`)
@@ -41,7 +41,7 @@ the `externLib.static` facet.
 It is an open type, meaning additional mappings can be add lazily
 as needed (via `target_data`).
 -/
-opaque TargetData (facet : WfName) : Type
+opaque TargetData (facet : Name) : Type
 
 /--
 The open type family which maps a custom target (package × target name) to
@@ -50,7 +50,7 @@ its build data in the Lake build store.
 It is an open type, meaning additional mappings can be add lazily
 as needed (via `custom_data`).
 -/
-opaque CustomData (target : WfName × WfName) : Type
+opaque CustomData (target : Name × Name) : Type
 
 --------------------------------------------------------------------------------
 /-! ## Build Data                                                             -/
@@ -75,28 +75,28 @@ abbrev BuildData : BuildKey → Type
 scoped macro (name := packageDataDecl) doc?:optional(Parser.Command.docComment)
 "package_data " id:ident " : " ty:term : command => do
   let dty := mkCIdentFrom (← getRef) ``PackageData
-  let key := WfName.quoteNameFrom id id.getId
+  let key := Lake.quoteNameFrom id id.getId
   `($[$doc?]? family_def $id : $dty $key := $ty)
 
 /-- Macro for declaring new `ModuleData`. -/
 scoped macro (name := moduleDataDecl) doc?:optional(Parser.Command.docComment)
 "module_data " id:ident " : " ty:term : command => do
   let dty := mkCIdentFrom (← getRef) ``ModuleData
-  let key := WfName.quoteNameFrom id id.getId
+  let key := Lake.quoteNameFrom id id.getId
   `($[$doc?]? family_def $id : $dty $key := $ty)
 
 /-- Macro for declaring new `TargetData`. -/
 scoped macro (name := targetDataDecl) doc?:optional(Parser.Command.docComment)
 "target_data " id:ident " : " ty:term : command => do
   let dty := mkCIdentFrom (← getRef) ``TargetData
-  let key := WfName.quoteNameFrom id id.getId
+  let key := Lake.quoteNameFrom id id.getId
   `($[$doc?]? family_def $id : $dty $key := $ty)
 
 /-- Macro for declaring new `CustomData`. -/
 scoped macro (name := customDataDecl) doc?:optional(Parser.Command.docComment)
 "custom_data " pkg:ident tgt:ident " : " ty:term : command => do
   let dty := mkCIdentFrom (← getRef) ``CustomData
   let id := mkIdentFrom tgt (pkg.getId ++ tgt.getId)
-  let pkg := WfName.quoteNameFrom pkg pkg.getId
-  let tgt := WfName.quoteNameFrom tgt tgt.getId
+  let pkg := Lake.quoteNameFrom pkg pkg.getId
+  let tgt := Lake.quoteNameFrom pkg tgt.getId
   `($[$doc?]? family_def $id : $dty ($pkg, $tgt) := $ty)

Lake/Build/Facets.lean

@@ -22,24 +22,24 @@ namespace Lake
 /-- A module facet name along with proof of its data type. -/
 structure ModuleFacet (α) where
   /-- The name of the module facet. -/
-  name : WfName
+  name : Name
   /-- Proof that module's facet build result is of type α. -/
   data_eq : ModuleData name = α
   deriving Repr
 
 instance (facet : ModuleFacet α) : FamilyDef ModuleData facet.name α :=
   ⟨facet.data_eq⟩
 
-instance [FamilyDef ModuleData facet α] : CoeDep WfName facet (ModuleFacet α) :=
+instance [FamilyDef ModuleData facet α] : CoeDep Name facet (ModuleFacet α) :=
   ⟨facet, family_key_eq_type⟩
 
 namespace Module
-abbrev leanBinFacet  := &`lean.bin
-abbrev oleanFacet    := &`olean
-abbrev ileanFacet    := &`ilean
-abbrev cFacet        := &`lean.c
-abbrev oFacet        := &`lean.o
-abbrev dynlibFacet   := &`dynlib
+abbrev leanBinFacet  := `lean.bin
+abbrev oleanFacet    := `olean
+abbrev ileanFacet    := `ilean
+abbrev cFacet        := `lean.c
+abbrev oFacet        := `lean.o
+abbrev dynlibFacet   := `dynlib
 end Module
 
 /--
@@ -72,11 +72,11 @@ package_data extraDep : ActiveOpaqueTarget
 
 -- ## Target Facets
 
-abbrev LeanLib.staticFacet := &`leanLib.static
-abbrev LeanLib.sharedFacet := &`leanLib.shared
-abbrev LeanExe.exeFacet := &`leanExe
-abbrev ExternLib.staticFacet := &`externLib.static
-abbrev ExternLib.sharedFacet := &`externLib.shared
+abbrev LeanLib.staticFacet := `leanLib.static
+abbrev LeanLib.sharedFacet := `leanLib.shared
+abbrev LeanExe.exeFacet := `leanExe
+abbrev ExternLib.staticFacet := `externLib.static
+abbrev ExternLib.sharedFacet := `externLib.shared
 
 /-- A Lean library's static binary. -/
 target_data leanLib.static : ActiveFileTarget

Lake/Build/Index.lean

@@ -27,21 +27,21 @@ namespace Lake
 
 /-- A map from module facet names to build functions. -/
 abbrev ModuleBuildMap (m : Type → Type v) :=
-  DRBMap WfName (cmp := WfName.quickCmp) fun k =>
+  DRBMap Name (cmp := Name.quickCmp) fun k =>
     Module → IndexBuildFn m → m (ModuleData k)
 
 @[inline] def ModuleBuildMap.empty : ModuleBuildMap m := DRBMap.empty
 
 /-- A map from package facet names to build functions. -/
 abbrev PackageBuildMap (m : Type → Type v) :=
-  DRBMap WfName (cmp := WfName.quickCmp) fun k =>
+  DRBMap Name (cmp := Name.quickCmp) fun k =>
     Package → IndexBuildFn m → m (PackageData k)
 
 @[inline] def PackageBuildMap.empty : PackageBuildMap m := DRBMap.empty
 
 /-- A map from target facet names to build functions. -/
 abbrev TargetBuildMap (m : Type → Type v) :=
-  DRBMap WfName (cmp := WfName.quickCmp) fun k =>
+  DRBMap Name (cmp := Name.quickCmp) fun k =>
     Package → IndexBuildFn m → m (PackageData k)
 
 @[inline] def TargetBuildMap.empty : PackageBuildMap m := DRBMap.empty
@@ -54,23 +54,23 @@ abbrev TargetBuildMap (m : Type → Type v) :=
 Converts a conveniently typed module facet build function into its
 dynamically typed equivalent.
 -/
-@[inline] def mkModuleFacetBuild {facet : WfName} (build : Module → IndexT m α)
+@[inline] def mkModuleFacetBuild {facet : Name} (build : Module → IndexT m α)
 [h : FamilyDef ModuleData facet α] : Module → IndexT m (ModuleData facet) :=
   cast (by rw [← h.family_key_eq_type]) build
 
 /--
 Converts a conveniently typed package facet build function into its
 dynamically typed equivalent.
 -/
-@[inline] def mkPackageFacetBuild {facet : WfName} (build : Package → IndexT m α)
+@[inline] def mkPackageFacetBuild {facet : Name} (build : Package → IndexT m α)
 [h : FamilyDef PackageData facet α] : Package → IndexT m (PackageData facet) :=
   cast (by rw [← h.family_key_eq_type]) build
 
 /--
 Converts a conveniently typed target facet build function into its
 dynamically typed equivalent.
 -/
-@[inline] def mkTargetFacetBuild (facet : WfName) (build : IndexT m α)
+@[inline] def mkTargetFacetBuild (facet : Name) (build : IndexT m α)
 [h : FamilyDef TargetData facet α] : IndexT m (TargetData facet) :=
   cast (by rw [← h.family_key_eq_type]) build
 
@@ -111,12 +111,12 @@ the initial set of Lake package facets (e.g., `extraDep`).
   have : MonadLift BuildM m := ⟨liftM⟩
   PackageBuildMap.empty (m := m)
   -- Compute the package's transitive dependencies
-  |>.insert &`deps (mkPackageFacetBuild <| fun pkg => do
+  |>.insert `deps (mkPackageFacetBuild <| fun pkg => do
     let mut deps := #[]
     let mut depSet := PackageSet.empty
     for dep in pkg.dependencies do
       if let some depPkg ← findPackage? dep.name then
-        for depDepPkg in (← recBuild <| depPkg.facet &`deps) do
+        for depDepPkg in (← recBuild <| depPkg.facet `deps) do
           unless depSet.contains depDepPkg do
             deps := deps.push depDepPkg
             depSet := depSet.insert depDepPkg
@@ -126,7 +126,7 @@ the initial set of Lake package facets (e.g., `extraDep`).
     return deps
   )
   -- Build the `extraDepTarget` for the package and its transitive dependencies
-  |>.insert &`extraDep (mkPackageFacetBuild <| fun pkg => do
+  |>.insert `extraDep (mkPackageFacetBuild <| fun pkg => do
     let mut target := ActiveTarget.nil
     for dep in pkg.dependencies do
       if let some depPkg ← findPackage? dep.name then

Lake/Build/IndexTargets.lean

@@ -12,7 +12,7 @@ namespace Lake
 
 -- # Module Facet Targets
 
-@[inline] def Module.facetTarget (facet : WfName) (self : Module)
+@[inline] def Module.facetTarget (facet : Name) (self : Module)
 [FamilyDef ModuleData facet (ActiveBuildTarget α)] : OpaqueTarget :=
   self.facet facet |>.target
 
@@ -35,7 +35,7 @@ Build the `extraDepTarget` of a package and its (transitive) dependencies
 and then build the target `facet` of library's modules recursively, constructing
 a single opaque target for the whole build.
 -/
-def LeanLib.buildModules (self : LeanLib) (facet : WfName)
+def LeanLib.buildModules (self : LeanLib) (facet : Name)
 [FamilyDef ModuleData facet (ActiveBuildTarget α)] : SchedulerM Job := do
   let buildMods : BuildM _ := do
     let mods ← self.getModuleArray

Lake/Build/Info.lean

@@ -20,28 +20,28 @@ namespace Lake
 
 /-- The type of Lake's build info. -/
 inductive BuildInfo
-| moduleFacet (module : Module) (facet : WfName)
-| packageFacet (package : Package) (facet : WfName)
+| moduleFacet (module : Module) (facet : Name)
+| packageFacet (package : Package) (facet : Name)
 | staticLeanLib (lib : LeanLib)
 | sharedLeanLib (lib : LeanLib)
 | leanExe (exe : LeanExe)
 | staticExternLib (lib : ExternLib)
 | sharedExternLib (lib : ExternLib)
-| customTarget (package : Package) (target : WfName)
+| customTarget (package : Package) (target : Name)
 
 --------------------------------------------------------------------------------
 /-! ## Build Info & Keys                                                      -/
 --------------------------------------------------------------------------------
 
 /-! ### Build Key Helper Constructors -/
 
-abbrev Module.facetBuildKey (facet : WfName) (self : Module) : BuildKey :=
+abbrev Module.facetBuildKey (facet : Name) (self : Module) : BuildKey :=
   .moduleFacet self.keyName facet
 
-abbrev Package.facetBuildKey (facet : WfName) (self : Package) : BuildKey :=
+abbrev Package.facetBuildKey (facet : Name) (self : Package) : BuildKey :=
   .packageFacet self.name facet
 
-abbrev Package.targetBuildKey (target : WfName) (self : Package) : BuildKey :=
+abbrev Package.targetBuildKey (target : Name) (self : Package) : BuildKey :=
   .customTarget self.name target
 
 abbrev LeanLib.staticBuildKey (self : LeanLib) : BuildKey :=
@@ -136,7 +136,7 @@ Defined here because they need to import configurations, whereas the definitions
 there need to be imported by configurations.
 -/
 
-abbrev Module.importFacet := &`lean.imports
+abbrev Module.importFacet := `lean.imports
 
 /-- The direct × transitive imports of the Lean module. -/
 module_data lean.imports : Array Module × Array Module
@@ -155,7 +155,7 @@ and target facets.
 namespace Module
 
 /-- Build info for the module's specified facet. -/
-abbrev facet (facet : WfName) (self : Module) : BuildInfo :=
+abbrev facet (facet : Name) (self : Module) : BuildInfo :=
   .moduleFacet self facet
 
 variable (self : Module)
@@ -171,15 +171,15 @@ abbrev dynlib   := self.facet dynlibFacet
 end Module
 
 /-- Build info for the package's specified facet. -/
-abbrev Package.facet (facet : WfName) (self : Package) : BuildInfo :=
+abbrev Package.facet (facet : Name) (self : Package) : BuildInfo :=
   .packageFacet self facet
 
 /-- Build info for the package's `extraDepTarget`. -/
 abbrev Package.extraDep (self : Package) : BuildInfo :=
-  self.facet &`extraDep
+  self.facet `extraDep
 
 /-- Build info for a custom package target. -/
-abbrev Package.customTarget (target : WfName) (self : Package) : BuildInfo :=
+abbrev Package.customTarget (target : Name) (self : Package) : BuildInfo :=
   .customTarget self target
 
 /-- Build info of the Lean library's static binary. -/

Lake/Build/Key.lean

@@ -9,10 +9,10 @@ namespace Lake
 
 /-- The type of keys in the Lake build store. -/
 inductive BuildKey
-| moduleFacet (module : WfName) (facet : WfName)
-| packageFacet (package : WfName) (facet : WfName)
-| targetFacet (package : WfName) (target : WfName) (facet : WfName)
-| customTarget (package : WfName) (target : WfName)
+| moduleFacet (module : Name) (facet : Name)
+| packageFacet (package : Name) (facet : Name)
+| targetFacet (package : Name) (target : Name) (facet : Name)
+| customTarget (package : Name) (target : Name)
 deriving Inhabited, Repr, DecidableEq, Hashable
 
 namespace BuildKey

Lake/Build/Roots.lean

@@ -90,7 +90,7 @@ def LeanExe.recBuild (self : LeanExe) : IndexT m ActiveFileTarget := do
     for facet in mod.nativeFacets do
       arr := arr.push <| Target.active <| ← recBuild <| mod.facet facet.name
     return arr
-  let deps := (← recBuild <| self.pkg.facet &`deps).push self.pkg
+  let deps := (← recBuild <| self.pkg.facet `deps).push self.pkg
   for dep in deps do for lib in dep.externLibs do
     linkTargets := linkTargets.push <| Target.active <| ← lib.static.recBuild
   leanExeTarget self.file linkTargets self.linkArgs |>.activate

Lake/Build/Store.lean

@@ -32,7 +32,7 @@ set_option linter.unusedVariables false
 
 /-- Derive an array of built module facets from the store. -/
 def collectModuleFacetArray (self : BuildStore)
-(facet : WfName) [FamilyDef ModuleData facet α] : Array α := Id.run do
+(facet : Name) [FamilyDef ModuleData facet α] : Array α := Id.run do
   let mut res : Array α := #[]
   for ⟨k, v⟩ in self do
     match k with
@@ -45,7 +45,7 @@ def collectModuleFacetArray (self : BuildStore)
 
 /-- Derive a map of module names to built facets from the store. -/
 def collectModuleFacetMap (self : BuildStore)
-(facet : WfName) [FamilyDef ModuleData facet α] : NameMap α := Id.run do
+(facet : Name) [FamilyDef ModuleData facet α] : NameMap α := Id.run do
   let mut res := Lean.mkNameMap α
   for ⟨k, v⟩ in self do
     match k with
@@ -58,7 +58,7 @@ def collectModuleFacetMap (self : BuildStore)
 
 /-- Derive an array of built package facets from the store. -/
 def collectPackageFacetArray (self : BuildStore)
-(facet : WfName) [FamilyDef PackageData facet α] : Array α := Id.run do
+(facet : Name) [FamilyDef PackageData facet α] : Array α := Id.run do
   let mut res : Array α := #[]
   for ⟨k, v⟩ in self do
     match k with
@@ -71,7 +71,7 @@ def collectPackageFacetArray (self : BuildStore)
 
 /-- Derive an array of built target facets from the store. -/
 def collectTargetFacetArray (self : BuildStore)
-(facet : WfName) [FamilyDef TargetData facet α] : Array α := Id.run do
+(facet : Name) [FamilyDef TargetData facet α] : Array α := Id.run do
   let mut res : Array α := #[]
   for ⟨k, v⟩ in self do
     match k with
@@ -84,5 +84,5 @@ def collectTargetFacetArray (self : BuildStore)
 
 /-- Derive an array of built external shared libraries from the store. -/
 def collectSharedExternLibs (self : BuildStore)
-[FamilyDef TargetData &`externLib.shared α] : Array α :=
-  self.collectTargetFacetArray &`externLib.shared
+[FamilyDef TargetData `externLib.shared α] : Array α :=
+  self.collectTargetFacetArray `externLib.shared