From d953ac8d0d1514b3d84d724ef4a6042213253c80 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 11 Jan 2022 09:50:09 -0800
Subject: [PATCH] feat: allow users to use `initialize
 registerBuiltinDerivingHandler ...`

---
 src/Lean/Elab/Deriving/Basic.lean               |  3 +--
 src/shell/CMakeLists.txt                        |  8 ++++++++
 tests/leanpkg/deriving/UserDeriving.lean        |  1 +
 tests/leanpkg/deriving/UserDeriving/Simple.lean | 15 +++++++++++++++
 tests/leanpkg/deriving/UserDeriving/Tst.lean    |  6 ++++++
 tests/leanpkg/deriving/leanpkg.toml             |  3 +++
 6 files changed, 34 insertions(+), 2 deletions(-)
 create mode 100644 tests/leanpkg/deriving/UserDeriving.lean
 create mode 100644 tests/leanpkg/deriving/UserDeriving/Simple.lean
 create mode 100644 tests/leanpkg/deriving/UserDeriving/Tst.lean
 create mode 100644 tests/leanpkg/deriving/leanpkg.toml

diff --git a/src/Lean/Elab/Deriving/Basic.lean b/src/Lean/Elab/Deriving/Basic.lean
index 7119a641e0aa..fef6b7456177 100644
--- a/src/Lean/Elab/Deriving/Basic.lean
+++ b/src/Lean/Elab/Deriving/Basic.lean
@@ -15,8 +15,7 @@ def DerivingHandlerNoArgs := (typeNames : Array Name) → CommandElabM Bool
 builtin_initialize derivingHandlersRef : IO.Ref (NameMap DerivingHandler) ← IO.mkRef {}
 
 def registerBuiltinDerivingHandlerWithArgs (className : Name) (handler : DerivingHandler) : IO Unit := do
-  let initializing ← IO.initializing
-  unless initializing do
+  unless (← initializing) do
     throw (IO.userError "failed to register deriving handler, it can only be registered during initialization")
   if (← derivingHandlersRef.get).contains className then
     throw (IO.userError s!"failed to register deriving handler, a handler has already been registered for '{className}'")
diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index 9e73f50efd00..e61d47f927da 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -182,6 +182,14 @@ add_test(NAME leanpkgtest_user_attr
            find . -name '*.olean' -delete
            leanmake")
 
+add_test(NAME leanpkgtest_user_deriving
+         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/deriving"
+         COMMAND bash -c "
+           set -eu
+           export ${TEST_VARS}
+           find . -name '*.olean' -delete
+           leanmake")
+
 add_test(NAME leanpkgtest_user_opt
          WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/user_opt"
          COMMAND bash -c "
diff --git a/tests/leanpkg/deriving/UserDeriving.lean b/tests/leanpkg/deriving/UserDeriving.lean
new file mode 100644
index 000000000000..92d1187af172
--- /dev/null
+++ b/tests/leanpkg/deriving/UserDeriving.lean
@@ -0,0 +1 @@
+import UserDeriving.Tst
diff --git a/tests/leanpkg/deriving/UserDeriving/Simple.lean b/tests/leanpkg/deriving/UserDeriving/Simple.lean
new file mode 100644
index 000000000000..23026e847a7c
--- /dev/null
+++ b/tests/leanpkg/deriving/UserDeriving/Simple.lean
@@ -0,0 +1,15 @@
+import Lean
+
+class Simple (α : Type u) where
+  val : α
+
+open Lean
+open Lean.Elab
+open Lean.Elab.Command
+def mkSimpleHandler (declNames : Array Name) : CommandElabM Bool := do
+  dbg_trace ">> mkSimpleHandler {declNames}"
+  -- TODO: see examples at src/Lean/Elab/Deriving
+  return true
+
+initialize
+  registerBuiltinDerivingHandler ``Simple mkSimpleHandler
diff --git a/tests/leanpkg/deriving/UserDeriving/Tst.lean b/tests/leanpkg/deriving/UserDeriving/Tst.lean
new file mode 100644
index 000000000000..51970ac3d99c
--- /dev/null
+++ b/tests/leanpkg/deriving/UserDeriving/Tst.lean
@@ -0,0 +1,6 @@
+import UserDeriving.Simple
+
+inductive Foo where
+  | mk₁
+  | mk₂
+  deriving Simple
diff --git a/tests/leanpkg/deriving/leanpkg.toml b/tests/leanpkg/deriving/leanpkg.toml
new file mode 100644
index 000000000000..bc4f17da39bb
--- /dev/null
+++ b/tests/leanpkg/deriving/leanpkg.toml
@@ -0,0 +1,3 @@
+[package]
+name = "UserDeriving"
+version = "0.1"