feat: allow users to use initialize registerBuiltinDerivingHandler ...

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}'")

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 "

tests/leanpkg/deriving/UserDeriving.lean

@@ -0,0 +1 @@
+import UserDeriving.Tst

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

tests/leanpkg/deriving/UserDeriving/Tst.lean

@@ -0,0 +1,6 @@
+import UserDeriving.Simple
+
+inductive Foo where
+  | mk₁
+  | mk₂
+  deriving Simple

tests/leanpkg/deriving/leanpkg.toml

@@ -0,0 +1,3 @@
+[package]
+name = "UserDeriving"
+version = "0.1"