From 34f7fa7a6d9184cccc7f0d29e9840820e4b29e38 Mon Sep 17 00:00:00 2001
From: "Alex J. Best" <alex.j.best@gmail.com>
Date: Mon, 18 Dec 2023 16:26:35 +0000
Subject: [PATCH] up

---
 Leaff/Diff.lean    | 28 +++++++++++++++++++++++++++-
 lake-manifest.json |  2 +-
 lean-toolchain     |  2 +-
 test/TestA.lean    |  3 +++
 test/TestB.lean    |  3 +++
 test/main.lean     |  4 ++++
 6 files changed, 39 insertions(+), 3 deletions(-)

diff --git a/Leaff/Diff.lean b/Leaff/Diff.lean
index 893ed43..0b83769 100644
--- a/Leaff/Diff.lean
+++ b/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
diff --git a/lake-manifest.json b/lake-manifest.json
index 28e0f79..9721595 100644
--- a/lake-manifest.json
+++ b/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",
diff --git a/lean-toolchain b/lean-toolchain
index 24a3cdb..91ccf6a 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.3.0-rc2
+leanprover/lean4:v4.4.0-rc1
diff --git a/test/TestA.lean b/test/TestA.lean
index 3b04714..484ab76 100644
--- a/test/TestA.lean
+++ b/test/TestA.lean
@@ -10,3 +10,6 @@ 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
index 9a820b1..827504d 100644
--- a/test/TestB.lean
+++ b/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
diff --git a/test/main.lean b/test/main.lean
index bffd668..49aa80b 100644
--- a/test/main.lean
+++ b/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