How does `@[derive]` choose the instance name?

Stream: general

[Eric Wieser]

I'm looking at src#instance_derive_handler but can't actually see where the name is being generated.

I ask because something like

@[derive [add_comm_group, vector_space ℝ]]
def foo (V : Type*) [inner_product_space ℝ V] : Type* := V × ℝ × ℝ

gives a lousy foo.inst name for the vector_space

[Rob Lewis]

src#tactic.delta_instance_handler

[Eric Wieser]

Is there an easy way to interactively ask lean to find everything tagged with derive_handler?

[Rob Lewis]

#eval attribute.get_instances `derive >>= tactic.trace ?

[Eric Wieser]

I guess ideally that derive handler would use heuristic_inst_name from the C++

[Eric Wieser]

#6007