update

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

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

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",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.8.0
+leanprover/lean4:v4.11.0-rc3

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

test/lake-manifest.json

@@ -1,4 +1,4 @@
-{"version": 7,
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages": [],
  "name": "test",

test/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.5.0-rc1
+leanprover/lean4:v4.11.0-rc3

test2/lake-manifest.json

@@ -1,5 +1,5 @@
-{"version": 7,
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages": [],
- "name": "test2",
+ "name": "test",
  "lakeDir": ".lake"}

test2/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.5.0-rc1
+leanprover/lean4:v4.11.0-rc3