tweaks and test setup

.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

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
+
 
 
 

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
 }

test/Test/Basic.lean

@@ -0,0 +1 @@
+def hello := "world"

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

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
 

test/lake-manifest.json

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

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]

test/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.5.0-rc1

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

test2/.gitignore

@@ -0,0 +1 @@
+/.lake

test2/Test/Basic.lean

@@ -0,0 +1 @@
+def hello := "world"

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

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

test2/lake-manifest.json

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

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

test2/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.5.0-rc1

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