diff --git a/.gitignore b/.gitignore
index 5afa42f..e7d6620 100644
--- a/.gitignore
+++ b/.gitignore
@@ -2,3 +2,11 @@
 /lake-packages/*
 lakefile.olean
 /.lake
+test/build
+test/.lake
+test/lake-packages/*
+test/lakefile.olean
+test2/build
+test2/.lake
+test2/lake-packages/*
+test2/lakefile.olean
diff --git a/Leaff/Diff.lean b/Leaff/Diff.lean
index ec9e49b..9de0b11 100644
--- a/Leaff/Diff.lean
+++ b/Leaff/Diff.lean
@@ -266,7 +266,7 @@ def summarize (diffs : List Diff) : MessageData := Id.run do
       | .typeChanged name _                             => m!"! type changed for {name}"
       | .speciesChanged name fro to _                   => m!"! {name} changed from {fro} to {to}"
       | .extensionEntriesModified ext                   => m!"! extension entry modified for {ext}"
-      | .docChanged name _                              => m!"! doc _  ified for {name}"
+      | .docChanged name _                              => m!"! doc modified for {name}"
       | .docAdded name _                                => m!"+ doc added to {name}"
       | .docRemoved name _                              => m!"- doc removed from {name}"
       | .moduleAdded name                               => m!"+ module added {name}"
@@ -319,7 +319,7 @@ def importDiffs (old new : Environment) : List Diff := Id.run do
 namespace PersistentEnvExtension
 
 def getImportedState [Inhabited α] (ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α)) (env : Environment) : NameMap α :=
-RBMap.fromArray ((ext.getState env).toList.toArray ++ (ext.toEnvExtension.getState env).importedEntries.flatten) Name.quickCmp
+RBMap.fromArray (ext.exportEntriesFn (ext.getState env) ++ (ext.toEnvExtension.getState env).importedEntries.flatten) Name.quickCmp
 
 -- TODO use mkStateFromImportedEntries maybe?
 end PersistentEnvExtension
@@ -540,7 +540,38 @@ def extDiffs (old new : Environment) (renames : NameMap Name) (ignoreInternal :
   -- let newexts := RBSet.ofList (new.constants.map₁.toList.map Prod.fst) Name.cmp -- TODO maybe quickCmp
   pure out
 
-  -- #check reducibilityAttrs
+-- Lean.namespacesExt
+-- Lean.protectedExt
+-- Lean.aliasExtension
+-- Lean.attributeExtension
+-- Lean.classExtension
+-- Lean.reducibilityAttrs
+-- Lean.Compiler.nospecializeAttr
+-- Lean.Compiler.specializeAttr
+-- Lean.externAttr
+-- Lean.Compiler.implementedByAttr
+-- Lean.neverExtractAttr
+-- Lean.exportAttr
+-- Lean.Compiler.CSimp.ext
+-- Lean.noncomputableExt
+-- Lean.Meta.globalInstanceExtension
+-- Lean.structureExt
+-- Lean.matchPatternAttr
+-- Lean.Meta.instanceExtension
+-- Lean.Meta.defaultInstanceExtension
+-- Lean.Meta.coeDeclAttr
+-- Lean.Linter.deprecatedAttr
+-- Lean.declRangeExt
+-- Lean.docStringExt
+-- Lean.moduleDocExt
+-- Lean.Meta.customEliminatorExt
+-- Lean.Elab.Term.elabWithoutExpectedTypeAttr
+-- Lean.Elab.Term.elabAsElim
+-- Lean.Meta.recursorAttribute
+-- Lean.Meta.simpExtension
+-- Lean.Meta.congrExtension
+-- Std.Tactic.Alias.aliasExt
+
 
 
 
diff --git a/lakefile.lean b/lakefile.lean
index 9a7e3e8..8004b6b 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -13,11 +13,6 @@ package «leaff» {
   -- add package configuration options here
 }
 
-lean_lib «test» {
-  globs := #[.submodules `test]
-  -- add library configuration options here
-}
-
 lean_lib «Leaff» {
   -- add library configuration options here
 }
diff --git a/test/Test/Basic.lean b/test/Test/Basic.lean
new file mode 100644
index 0000000..e99d3a6
--- /dev/null
+++ b/test/Test/Basic.lean
@@ -0,0 +1 @@
+def hello := "world"
\ No newline at end of file
diff --git a/test/Test/Test.lean b/test/Test/Test.lean
new file mode 100644
index 0000000..8c61a3b
--- /dev/null
+++ b/test/Test/Test.lean
@@ -0,0 +1,35 @@
+
+/-- has a doc -/
+def a : Nat := 1
+
+def c : Nat := 1
+def bloop : Nat := 1
+
+theorem sada : Int := 123
+
+
+structure blah where
+  (a b : Nat)
+
+/-- magic number-/
+def hasdoc : Int := 123
+
+
+
+class blasdf where
+  (a b : Nat)
+
+
+def floo : blasdf := ⟨1, 2⟩
+
+
+
+theorem bloop1 : 3 ≠ 9 := by decide
+
+
+
+def defToLemma : 1 = 1 := rfl
+
+set_option pp.all true
+#print bloop1
+-- #eval Leaff.printHashes ``bloop1
diff --git a/test/TestA.lean b/test/TestA.lean
deleted file mode 100644
index 484ab76..0000000
--- a/test/TestA.lean
+++ /dev/null
@@ -1,15 +0,0 @@
-
-
-/-- has a doc -/
-def a : Nat := 1
-
-def c : Nat := 1
-
-theorem sada : Int := 123
-
-
-structure blah where
-  (a b : Nat)
-
-/-- magic number-/
-def hasdoc : Int := 123
diff --git a/test/TestB.lean b/test/TestB.lean
deleted file mode 100644
index 827504d..0000000
--- a/test/TestB.lean
+++ /dev/null
@@ -1,15 +0,0 @@
-
-def a : Nat := 1
-
-def b : Nat := 1
-
-def c : Nat := 2
-
-def sada : Int := 123
-
-
-class blah where
-  (a b : Nat)
-
-/-- not so magic number-/
-def hasdoc : Int := 123
diff --git a/test/diffin.lean b/test/diffin.lean
index 1b45684..9f0a6f0 100644
--- a/test/diffin.lean
+++ b/test/diffin.lean
@@ -18,6 +18,11 @@ diff in
 /-- ik heb een docstring -/
 def aaa : LE Nat := sorry
 
+structure Foo where
+  x : Nat
+  y : Nat
+diff in
+attribute [class] Foo
 diff in
 attribute [instance] aaa
 
diff --git a/test/lake-manifest.json b/test/lake-manifest.json
new file mode 100644
index 0000000..43b7832
--- /dev/null
+++ b/test/lake-manifest.json
@@ -0,0 +1,5 @@
+{"version": 7,
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "test",
+ "lakeDir": ".lake"}
diff --git a/test/lakefile.lean b/test/lakefile.lean
new file mode 100644
index 0000000..8c2430c
--- /dev/null
+++ b/test/lakefile.lean
@@ -0,0 +1,8 @@
+import Lake
+open Lake DSL
+
+package «test» where
+  -- add package configuration options here
+
+lean_lib «Test» where
+  globs := #[.submodules `Test]
diff --git a/test/lean-toolchain b/test/lean-toolchain
new file mode 100644
index 0000000..3f21e50
--- /dev/null
+++ b/test/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.5.0-rc1
diff --git a/test/main.lean b/test/main.lean
index 49aa80b..2468c24 100644
--- a/test/main.lean
+++ b/test/main.lean
@@ -4,12 +4,9 @@ import Lean
 open Lean
 
 def sp : SearchPath :=
-["."/".lake" /"build"/"lib","."/".lake" /"packages"/"std"/"build"/"lib","/home/alexanderbest/.elan/toolchains/leanprover--lean4---v4.3.0-rc2/lib/lean"]
+["."/".lake" /"build"/"lib","."/".lake" /"packages"/"std"/"build"/"lib","/home/alexanderbest/.elan/toolchains/leanprover--lean4---v4.4.0-rc1/lib/lean"]
 
 #eval summarizeDiffImports #[`Std.Classes.RatCast] #[`Std.Data.Rat] sp sp
 -- #eval summarizeDiffImports #[`Mathlib] #[`Mathlib] sp₁ sp₂
 
-#eval summarizeDiffImports #[`test.TestA] #[`test.TestB] sp sp
-
-open private docStringExt in Lean.findDocString?
-#check docStringExt
+#eval summarizeDiffImports #[`test.TestA] #[`test2.Test] sp sp
diff --git a/test2/.gitignore b/test2/.gitignore
new file mode 100644
index 0000000..bfb30ec
--- /dev/null
+++ b/test2/.gitignore
@@ -0,0 +1 @@
+/.lake
diff --git a/test2/Test/Basic.lean b/test2/Test/Basic.lean
new file mode 100644
index 0000000..e99d3a6
--- /dev/null
+++ b/test2/Test/Basic.lean
@@ -0,0 +1 @@
+def hello := "world"
\ No newline at end of file
diff --git a/test2/Test/Test.lean b/test2/Test/Test.lean
new file mode 100644
index 0000000..5497d6d
--- /dev/null
+++ b/test2/Test/Test.lean
@@ -0,0 +1,27 @@
+def a : Nat := 1
+
+def b : Nat := 1
+
+-- value changed
+def c : Nat := 2
+
+def sada : Int := 123
+
+
+class blah where
+  (a b : Nat)
+
+/-- not so magic number-/
+def hasdoc : Int := 123
+
+
+class blasdf where
+  (a b : Nat)
+
+instance floo : blasdf := ⟨1, 2⟩
+
+theorem bloop2 : 3 ≠ 9 := by decide
+
+theorem defToLemma : 1 = 1 := rfl
+
+-- #eval Leaff.printHashes ``bloop2
diff --git a/test2/hashset.lean b/test2/hashset.lean
new file mode 100644
index 0000000..49a3328
--- /dev/null
+++ b/test2/hashset.lean
@@ -0,0 +1,8 @@
+import Leaff.HashSet
+
+open Lean
+#eval (mkHashSet.insertMany [3,4,5,6,7,8,9,0,1,4,6,213,2432,435,435,234,12,2]).numBuckets
+#eval (mkHashSet.insertMany [3,21343245,213131,4,5,6,7,8,9,0,1,4,6,213,2432,435,435,234,12,2]).numBuckets
+#eval (mkHashSet.insertMany [1]).numBuckets
+#eval (mkHashSet.insertMany [3,4,5,6,7,8,9,0,1,4,6,213,2432,435,435,234,12,2,12312,12321] |>.sdiff (mkHashSet.insertMany [1,2,3])).toList
+#eval (mkHashSet.insertMany [3,4] |>.sdiff (mkHashSet.insertMany [1,2,3])).toList
diff --git a/test2/lake-manifest.json b/test2/lake-manifest.json
new file mode 100644
index 0000000..77b9f81
--- /dev/null
+++ b/test2/lake-manifest.json
@@ -0,0 +1,5 @@
+{"version": 7,
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "test2",
+ "lakeDir": ".lake"}
diff --git a/test2/lakefile.lean b/test2/lakefile.lean
new file mode 100644
index 0000000..1ecc7a7
--- /dev/null
+++ b/test2/lakefile.lean
@@ -0,0 +1,9 @@
+import Lake
+open Lake DSL
+
+package «test» where
+  -- add package configuration options here
+
+lean_lib «Test» where
+  globs := #[.submodules `Test]
+  -- add library configuration options here
diff --git a/test2/lean-toolchain b/test2/lean-toolchain
new file mode 100644
index 0000000..3f21e50
--- /dev/null
+++ b/test2/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.5.0-rc1
diff --git a/test2/main.lean b/test2/main.lean
new file mode 100644
index 0000000..6f23d25
--- /dev/null
+++ b/test2/main.lean
@@ -0,0 +1,12 @@
+import Leaff.Diff
+import Lean
+
+open Lean
+
+def sp : SearchPath :=
+["."/".lake" /"build"/"lib","."/".lake" /"packages"/"std"/"build"/"lib","/home/alexanderbest/.elan/toolchains/leanprover--lean4---v4.4.0-rc1/lib/lean"]
+
+#eval summarizeDiffImports #[`Std.Classes.RatCast] #[`Std.Data.Rat] sp sp
+-- #eval summarizeDiffImports #[`Mathlib] #[`Mathlib] sp₁ sp₂
+
+#eval summarizeDiffImports #[`test.TestA] #[`test.TestB] sp sp