Derive handlers

Stream: lean4

[Simon Hudon]

I'm trying to write a derive handler for my class. If I minimize my example, I get this:

def mkCLIArgRecordInstanceHandler : Array Name → CommandElabM Bool
| #[t] => do
  return true
| _ => do
  return false

builtin_initialize
  Lean.Elab.registerBuiltinDerivingHandler `CLIArgRecord
    mkCLIArgRecordInstanceHandler

structure Foo where
  field1 := false
  deriving CLIArgRecord
-- default handlers have not been implemented yet, class: 'CLIArgRecord' types: [CLI.Derive.Foo]

I get an error on the declaration of Foo even if I move it to a separate file, I get the same error. What am I missing?

[Arthur Paulino]

Can you add the imports too?

[Simon Hudon]

Certainly:

import Lean.Elab.Deriving.Basic
import Lean.Elab.Deriving.Util
import Lean.PrettyPrinter.Delaborator.Basic
import Std.Data.HashMap

but I think only

import Lean.Elab.Deriving.Basic
import Lean.Elab.Deriving.Util

are relevant

[Arthur Paulino]

Where is CLIArgRecord? I couldn't find it on the Lean 4 repo

[Simon Hudon]

It's my definition, sorry

[Simon Hudon]

inductive StreamReader (α : Type u) (β : Type v) where
  | read (f : α → StreamReader α β) : StreamReader α β
  | pure : β → StreamReader α β
  | error : String → StreamReader α β

class CLIArgRecord (α : Type u) where
  init : α
  parse : String → α → Option (StreamReader String α)
  usageString : String

[Simon Hudon]

Is this relevant to the derive handler working or not?

[Arthur Paulino]

I'm not sure... I just wanted to get rid of the unknown constant 'CLIArgRecord' error

[Simon Hudon]

Maybe an empty class would be sufficient

[Arthur Paulino]

Ah, seems like you're hitting a temporary dead end here

[Arthur Paulino]

That function just throws the exception right away

[Simon Hudon]

It is called here If the handler is found or if it returns true, that shouldn't happen

[Simon Hudon]

Actually, it's probably the other branch. If the handler returns true unconditionally, we should see something happening. For some reason, the handler doesn't make it into the table or it's not found when I look it up

[Simon Hudon]

My builtin_initialize block doesn't seem to get run. Is it something I have to use from a separate package?

[Arthur Paulino]

Searching for calls of registerBuiltinDerivingHandler in the Lean 4 repo, sometimes it's followed by a call to registerTraceClass. I'm not sure if it's related though

[Simon Hudon]

It shouldn't be. That's just for registering tags for tracing. If you register myTag, then set_option trace.myTag true with turn on the printing of information where you used that tag.

[Arthur Paulino]

Simon Hudon said:

My builtin_initialize block doesn't seem to get run. Is it something I have to use from a separate package?

My guess is that it has something to do with building before being able to use it

[Arthur Paulino]

From my experience when dealing with the FFI, this line doesn't do much on the Lean 4 server. It only does something when my code is built and I run it

[Arthur Paulino]

In the context of my repo, however, init is a constant marked with extern "nl_initialize", so that can very well be why I need to build it first.

[Simon Hudon]

But if you do lake build, does it get run?

[Arthur Paulino]

It definitely runs when I call ./bla (the executable file)

[Simon Hudon]

Because derive handler requires builtin_initialize, I'm wondering if I need a stricter separation, like using the derive handler as a plugin. @Sebastian Ullrich, would you care to shed some light here?

[Mac]

@Simon Hudon are you sure you can't just use initialize? Despite their names, many of the functions with Builtin in the name do not actually require a buitlin_initialize.

[Simon Hudon]

Yes, here's the error I get:

././Main.lean:2:0: error: failed to register deriving handler, it can only be registered during initialization

[Mario Carneiro]

Isn't this just the usual issue with builtin_initialize? You can't use it in the same file it is defined. Try putting the example inductive in another file

[Arthur Paulino]

He mentioned that he tried that

[Sebastian Ullrich]

builtin_initialize is run in executables and plugins only. It would be good to have a regular attribute for registering non-builtin derive handlers.

[Simon Hudon]

Ok so if I write a derive handler in a library, I need to load that library as a plugin. Does lake allow me to do that?

[Leonardo de Moura]

@Simon Hudon Pushed https://github.com/leanprover/lean4/commit/d953ac8d0d1514b3d84d724ef4a6042213253c80
It contains a small example. Not fully tested, if you find problems, please create an issue on GitHub.

[Simon Hudon]

Great! That's really helpful! Thank you

[Simon Hudon]

update: @Leonardo de Moura I tried it and it works like a charm! Thanks again!

[Arthur Paulino]

(deleted)