diff --git a/Leaff/Diff.lean b/Leaff/Diff.lean
index a2e0b35..efdab58 100644
--- a/Leaff/Diff.lean
+++ b/Leaff/Diff.lean
@@ -1,6 +1,5 @@
 import Lean
 import Batteries.Lean.PersistentHashSet
-import Batteries.Lean.Name
 import Batteries.Tactic.OpenPrivate
 -- import Leaff.Deriving.Optics
 import Leaff.Hash
@@ -393,7 +392,7 @@ instance : ToString ReducibilityStatus where
     | ReducibilityStatus.semireducible => "semireducible"
     | ReducibilityStatus.irreducible => "irreducible"
 
-open private docStringExt in Lean.findDocString?
+open private docStringExt in Lean.findSimpleDocString?
 
 /-- Take the diff between an old and new state of some environment extension,
 at the moment we hardcode the extensions we are interested in, as it is not clear how we can go beyond that. -/
@@ -621,7 +620,7 @@ def constantDiffs (old new : Environment) (ignoreInternal : Bool := true) : List
   --   old.insert ha <| (old.findD ha #[]).push name) (mkRBMap UInt64 (Array Name) Ord.compare) old.constants)
   -- sz is roughly how many non-internal decls we expect, empirically around 1/4th of total
   -- TODO change if internals included
-  let sz := max (new.constants.size / 4) (old.constants.size / 4)
+  let sz := max (new.constants.fold (fun x y z => x + 1) 0 / 4) (old.constants.fold (fun x y z => x + 1) 0 / 4)
 
   -- first we make a hashmap of all decls, hashing with `diffHash`, this should cut the space of "interesting" decls down drastically
   -- TODO reconsider internals, how useful are they
@@ -818,5 +817,5 @@ diffs in
 @[deprecated]
 noncomputable
 def a:=1
--- diffs in
--- attribute [reducible] a
+diffs in
+attribute [reducible] a
diff --git a/README.md b/README.md
index fd6e79f..e45fc10 100644
--- a/README.md
+++ b/README.md
@@ -17,6 +17,11 @@ build both by running `lake build` in the corresponding directories, then naviga
 ```
 note that the module name will likely just be the name of the library (e.g. `Mathlib`) if want to know all potential downstream changes of some change, but could be more specific, e.g. `MyLibrary.SomeFile`. The paths could be relative to the Leaff directory or absolute.
 
+E.g. to test from this directory
+```
+./runleaff.sh Test.Test test test2
+```
+
 You may face many issues, especially if the diff is too big, if there are different Lean versions use in the libraries, or if there is a different Lean version used to compile the libraries and Leaff itself.
 
 ```diff
diff --git a/lake-manifest.json b/lake-manifest.json
index 3466d2e..4f0b0b5 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,19 +1,19 @@
-{"version": 7,
+{"version": "1.0.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover/lean4-cli.git",
    "type": "git",
    "subDir": null,
-   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
+   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": false,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries.git",
    "type": "git",
    "subDir": null,
-   "rev": "3b1555252d9369be7b0f39a0e0a07daa864e5b5b",
+   "rev": "a7fd140a94bbbfa40cf10839227bbb9e8492be2d",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lean-toolchain b/lean-toolchain
index ef1f67e..1e6f28e 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.8.0
+leanprover/lean4:v4.11.0-rc3
\ No newline at end of file
diff --git a/test/Test/Test.lean b/test/Test/Test.lean
index 8c61a3b..3634e7f 100644
--- a/test/Test/Test.lean
+++ b/test/Test/Test.lean
@@ -5,7 +5,7 @@ def a : Nat := 1
 def c : Nat := 1
 def bloop : Nat := 1
 
-theorem sada : Int := 123
+-- theorem sada : Int := 123
 
 
 structure blah where
diff --git a/test/lake-manifest.json b/test/lake-manifest.json
index 43b7832..13ed49c 100644
--- a/test/lake-manifest.json
+++ b/test/lake-manifest.json
@@ -1,4 +1,4 @@
-{"version": 7,
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages": [],
  "name": "test",
diff --git a/test/lean-toolchain b/test/lean-toolchain
index 3f21e50..1e6f28e 100644
--- a/test/lean-toolchain
+++ b/test/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.5.0-rc1
+leanprover/lean4:v4.11.0-rc3
\ No newline at end of file
diff --git a/test2/lake-manifest.json b/test2/lake-manifest.json
index 77b9f81..13ed49c 100644
--- a/test2/lake-manifest.json
+++ b/test2/lake-manifest.json
@@ -1,5 +1,5 @@
-{"version": 7,
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages": [],
- "name": "test2",
+ "name": "test",
  "lakeDir": ".lake"}
diff --git a/test2/lean-toolchain b/test2/lean-toolchain
index 3f21e50..1e6f28e 100644
--- a/test2/lean-toolchain
+++ b/test2/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.5.0-rc1
+leanprover/lean4:v4.11.0-rc3
\ No newline at end of file