up

Leaff/Diff.lean

@@ -231,6 +231,7 @@ instance [BEq α] [Hashable α] : ForIn m (SMap α β) (α × β) where
   forIn t init f := do
     forIn t.map₂ (← forIn t.map₁ init f) f
 
+open private docStringExt in Lean.findDocString?
 /-- Copied from `whatsnew` by @gebner and heavily cannibalized -/
 def diffExtension (old new : Environment)
     (ext : PersistentEnvExtension EnvExtensionEntry EnvExtensionEntry EnvExtensionState) :
@@ -245,9 +246,34 @@ def diffExtension (old new : Environment)
   let newEntries := ext.exportEntriesFn newSt
   -- dbg_trace oldEntries.size
   -- dbg_trace newEntries.size
+  -- dbg_trace ext.name
   let mut out := []
   match ext.name with
-  | ``Lean.classExtension => do
+  | `Lean.docStringExt => do
+      dbg_trace "doc"
+      dbg_trace (SimplePersistentEnvExtension.getState docStringExt new).toList
+      for (a, b) in SimplePersistentEnvExtension.getState docStringExt new do
+        if ¬ (SimplePersistentEnvExtension.getState docStringExt old).contains a then
+          out := .docAdded a :: out
+        else
+          if (SimplePersistentEnvExtension.getState docStringExt old).find! a != b then
+            out := .docChanged a :: out
+      for (a, _b) in SimplePersistentEnvExtension.getState docStringExt old do
+        if ¬ (SimplePersistentEnvExtension.getState docStringExt new).contains a then
+          out := .docRemoved a :: out
+  | `Lean.classExtension => do
+      dbg_trace "doc"
+      dbg_trace (SimplePersistentEnvExtension.getState classExtension new).outParamMap.toList
+      -- for (a, b) in SimplePersistentEnvExtension.getState docStringExt new do
+      --   if ¬ (SimplePersistentEnvExtension.getState docStringExt old).contains a then
+      --     out := .docAdded a :: out
+      --   else
+      --     if (SimplePersistentEnvExtension.getState docStringExt old).find! a != b then
+      --       out := .docChanged a :: out
+      -- for (a, _b) in SimplePersistentEnvExtension.getState docStringExt old do
+      --   if ¬ (SimplePersistentEnvExtension.getState docStringExt new).contains a then
+      --     out := .docRemoved a :: out
+  | `Lean.classExtensin => do
       -- for mod in [0:old.header.moduleData.size] do
         -- (ext.getModuleEntries old mod)
       -- IO.println (ext.getModuleEntries old mod).size

lake-manifest.json

@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover/std4.git",
    "type": "git",
    "subDir": null,
-   "rev": "d3049643f6dded69eb7ce8124796cb1ec8df8840",
+   "rev": "fadefd5a532a774dc47d00f9fa0bce3dc47ba2e1",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.3.0-rc2
+leanprover/lean4:v4.4.0-rc1

test/TestA.lean

@@ -10,3 +10,6 @@ theorem sada : Int := 123
 
 structure blah where
   (a b : Nat)
+
+/-- magic number-/
+def hasdoc : Int := 123

test/TestB.lean

@@ -10,3 +10,6 @@ def sada : Int := 123
 
 class blah where
   (a b : Nat)
+
+/-- not so magic number-/
+def hasdoc : Int := 123

test/main.lean

@@ -1,4 +1,5 @@
 import Leaff.Diff
+import Lean
 
 open Lean
 
@@ -9,3 +10,6 @@ def sp : SearchPath :=
 -- #eval summarizeDiffImports #[`Mathlib] #[`Mathlib] sp₁ sp₂
 
 #eval summarizeDiffImports #[`test.TestA] #[`test.TestB] sp sp
+
+open private docStringExt in Lean.findDocString?
+#check docStringExt