deriving extensions

Stream: lean4

[Leonardo de Moura]

Users will be able to extend deriving for their own classes. However, deriving is a relatively new feature, and the API is not stable and there are missing features. That being said, users should be able to invoke registerBuiltinDerivingHandler from their plugins. You can build a plugin containing

def mkMyClassInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
  ...

initialize
  registerBuiltinDerivingHandler `MyClass mkMyClassInstanceHandler

Disclaimer: we do not have many tests for Lean 4 plugins yet, and we never extended deriving using plugins :(
We have a very simple plugin at lean4/tests/plugin.