From cffc77d14751c3ae157716b8fd4f041641839306 Mon Sep 17 00:00:00 2001
From: ammkrn <chris@christopherabailey.com>
Date: Sun, 25 Jan 2026 17:45:08 -0800
Subject: [PATCH] fix: handle malformed declars from attributes

Some attributes like to_additive and to_dual create declarations which
do not preserve the property that their `all` list is "a List of all
(including this one) declarations in the same mutual block." The current
thmeorem/def/opaque export logic relied on this being the case for
all declarations.

This fix ensures that the current "base" declaration is included in
the list of names exported, and tries to ensure declarations are not
re-exported by the appearance of malformed declarations, for example if:

+ declaration `x` has an `all` list `[x]`, and;
+ declaration `y` has an  `all` list of `[x]`

then the old/current logic would export `x` twice if it was found
first; once for the `x` declaration, and again when exporting `y`.

Ideally there would be an upstream change to try and ensure that this
invariant is preserved, but the exporter should probably be made robust
against this either way.
---
 Export.lean                  | 12 +++++++-----
 Main.lean                    |  2 +-
 examples/Nat.add_succ.ndjson |  2 +-
 3 files changed, 9 insertions(+), 7 deletions(-)

diff --git a/Export.lean b/Export.lean
index c560ab2..c73543c 100644
--- a/Export.lean
+++ b/Export.lean
@@ -366,11 +366,13 @@ where
   theorems and definitions/opaques are still dumped in a singleton array for simplicity. -/
   dumpThmDefOpaque (base : ConstantInfo) : M Unit := do
     let mut all := #[]
-    for declarName in base.all do
-      let declar := (← read).env.find? declarName |>.get!
-      assert!((!declar.isUnsafe) || (← get).exportUnsafe)
-      all := all.push declar
-      modify fun st => { st with visitedConstants:= st.visitedConstants.insert declarName }
+    for declarName in (if base.all.contains base.name then base.all else base.name :: base.all) do
+      if declarName == base.name || !(← get).visitedConstants.contains declarName
+      then
+        let declar := (← read).env.find? declarName |>.get!
+        assert!((!declar.isUnsafe) || (← get).exportUnsafe)
+        all := all.push declar
+        modify fun st => { st with visitedConstants:= st.visitedConstants.insert declarName }
     for declar in all do
       dumpDeps declar.type
       dumpDeps (declar.value! (allowOpaque := true))
diff --git a/Main.lean b/Main.lean
index 455ebcf..a75e9db 100644
--- a/Main.lean
+++ b/Main.lean
@@ -8,7 +8,7 @@ def exportMetadata : Json :=
   ]
   let exporterMeta := Json.mkObj [
     ("name", "lean4export"),
-    ("version", "3.0.0")
+    ("version", "3.1.0")
   ]
   let formatMeta := Json.mkObj [
     ("version", "3.0.0")
diff --git a/examples/Nat.add_succ.ndjson b/examples/Nat.add_succ.ndjson
index d3cd35f..558af1b 100644
--- a/examples/Nat.add_succ.ndjson
+++ b/examples/Nat.add_succ.ndjson
@@ -1,4 +1,4 @@
-{"meta":{"exporter":{"name":"lean4export","version":"3.0.0"},"format":{"version":"3.0.0"},"lean":{"githash":"2fcce7258eeb6e324366bc25f9058293b04b7547","version":"4.27.0-rc1"}}}
+{"meta":{"exporter":{"name":"lean4export","version":"3.0.0"},"format":{"version":"3.0.0"},"lean":{"githash":"db93fe1608548721853390a10cd40580fe7d22ae","version":"4.27.0"}}}
 {"in":1,"str":{"pre":0,"str":"Nat"}}
 {"il":1,"succ":0}
 {"ie":0,"sort":1}