fix: make structure parent info persist (leanprover#5890)

Modifies the `structureExt` from being a `SimplePersistentEnvExtension`
to a `PersistentEnvExtension`. The simple version contains a `List` of
all added entries, which we do not need since we already have a
`PersistentHashMap` of them in the state. The oversight was that this
`List` contained duplicate entries due to `setStructureParents`
re-adding entries.

src/Lean/Structure.lean

@@ -80,10 +80,11 @@ private structure StructureState where
   map : PersistentHashMap Name StructureInfo := {}
   deriving Inhabited
 
-builtin_initialize structureExt : SimplePersistentEnvExtension StructureInfo StructureState ← registerSimplePersistentEnvExtension {
-  addImportedFn := fun _ => {}
-  addEntryFn    := fun s e => { s with map := s.map.insert e.structName e }
-  toArrayFn     := fun es => es.toArray.qsort StructureInfo.lt
+builtin_initialize structureExt : PersistentEnvExtension StructureInfo StructureInfo (Unit × StructureState) ← registerPersistentEnvExtension {
+  mkInitial       := pure ((), {})
+  addImportedFn   := fun _ => pure ((), {})
+  addEntryFn      := fun (_, s) e => ((), { s with map := s.map.insert e.structName e })
+  exportEntriesFn := fun (_, s) => s.map.toArray |>.map (·.snd) |>.qsort StructureInfo.lt
 }
 
 /--
@@ -113,15 +114,15 @@ Set parent projection info for a structure defined in the current module.
 Throws an error if the structure has not already been registered with `Lean.registerStructure`.
 -/
 def setStructureParents [Monad m] [MonadEnv m] [MonadError m] (structName : Name) (parentInfo : Array StructureParentInfo) : m Unit := do
-  let some info := structureExt.getState (← getEnv) |>.map.find? structName
+  let some info := structureExt.getState (← getEnv) |>.snd.map.find? structName
     | throwError "cannot set structure parents for '{structName}', structure not defined in current module"
   modifyEnv fun env => structureExt.addEntry env { info with parentInfo }
 
 /-- Gets the `StructureInfo` if `structName` has been declared as a structure to the elaborator. -/
 def getStructureInfo? (env : Environment) (structName : Name) : Option StructureInfo :=
   match env.getModuleIdxFor? structName with
   | some modIdx => structureExt.getModuleEntries env modIdx |>.binSearch { structName } StructureInfo.lt
-  | none        => structureExt.getState env |>.map.find? structName
+  | none        => structureExt.getState env |>.snd.map.find? structName
 
 /--
 Gets the `StructureInfo` for `structName`, which is assumed to have been declared as a structure to the elaborator.