Zulip Chat Archive

Stream: general

Topic: derive handler for fintype


view this post on Zulip Scott Morrison (Mar 04 2020 at 20:05):

@Simon Hudon, I notice that in archive/sensitivity.lean we successfully use a @[derive fintype]. Where is this coming from? I want to use it somewhere else but can't work out what I need to import. I just get a failed to find a derive handler for fintype message.

view this post on Zulip Scott Morrison (Mar 04 2020 at 20:08):

Related derive question... It seems there's a problem if you use @[derive decidable_eq] twice in the same file, and there is a broken work-around in place.

view this post on Zulip Scott Morrison (Mar 04 2020 at 20:09):

The problem seems to be disambiguating the decidable_eq in the second @[derive decidable_eq] annotation. Does that mean _root_.decidable_eq, or is it just the instance that was defined a moment ago by the first derive handler? (Which has a name ending in decidable_eq!)

view this post on Zulip Scott Morrison (Mar 04 2020 at 20:10):

The error message that shows up is failed to find a derive handler for 'choice decidable_eq category_theory.limits.walking_parallel_pair.decidable_eq'

view this post on Zulip Simon Hudon (Mar 04 2020 at 20:10):

To find the fintype derive handler, try: run_cmd attribute.get_instances `derive_handler >>= tactic.trace

view this post on Zulip Scott Morrison (Mar 04 2020 at 20:10):

And I'm guessing (?) that this choice business is some attempt to work out what we're actually trying to derive, based on what's actually available?

view this post on Zulip Simon Hudon (Mar 04 2020 at 20:12):

choice I believe is the Lean macro for name overloading. It defers to the elaborator the choice between the two. But that being said, it's curious that it would affect you there.

view this post on Zulip Simon Hudon (Mar 04 2020 at 20:16):

I think I see the problem. This is the parser for the derive attribute: parser := pexpr_list_or_texpr. It has to parse expressions because you could specify something like module real

view this post on Zulip Simon Hudon (Mar 04 2020 at 20:17):

If you give a name to the offending decidable_eq instance, that should go away

view this post on Zulip Simon Hudon (Mar 04 2020 at 20:17):

(a name different from decidable_eq

view this post on Zulip Reid Barton (Mar 04 2020 at 20:19):

which you can't do because it was generated automatically by the derive handler

view this post on Zulip Simon Hudon (Mar 04 2020 at 20:19):

Actually, we may be able to make that code a bit more robust

view this post on Zulip Scott Morrison (Mar 04 2020 at 20:29):

okay... I have a PR I'm looking at that has @[derive _root_.decidable_eq] to get around this problem. Should I allow that for now, or better to wait on some robustification?

view this post on Zulip Simon Hudon (Mar 04 2020 at 20:34):

I think you should keep that PR. The change would go in Lean itself

view this post on Zulip Simon Hudon (Mar 04 2020 at 20:45):

There are two ways to fix your particular issue. Either we generate a different name for the instance or we tolerate ambiguities in the name of the classes that we're trying to build an instance for

view this post on Zulip Simon Hudon (Mar 04 2020 at 20:47):

The solution for both is very simple. I'm not sure about the ramifications though

view this post on Zulip Rob Lewis (Mar 04 2020 at 20:48):

Note that the delta_instance handler (which just unfolds a definition and calls apply_instance) appends something to the name for exactly this reason. https://github.com/leanprover-community/mathlib/blob/master/src/tactic/core.lean#L1511

view this post on Zulip Simon Hudon (Mar 04 2020 at 20:52):

If you use it twice in a row and that it generates an instance for the same class, will you have a name clash with that approach?

view this post on Zulip Rob Lewis (Mar 04 2020 at 20:53):

The name is based on the type and the instance it's looking for, and it uses get_unused_decl_name, so no, I hope not.

view this post on Zulip Simon Hudon (Mar 04 2020 at 21:04):

That might be the right approach then. We could move get_unused_decl_name to core for that

view this post on Zulip Rob Lewis (Mar 04 2020 at 21:06):

Huh, I kind of assumed get_unused_decl_name was from core already, guess not.

view this post on Zulip Simon Hudon (Mar 04 2020 at 21:16):

Me too. That means that it shouldn't clash too much with its new neighbors

view this post on Zulip Simon Hudon (Mar 04 2020 at 21:22):

It would be nice if the meta programming interface allowed us to make protected declarations

view this post on Zulip Rob Lewis (Mar 04 2020 at 21:22):

Absolutely, I've wanted that a whole bunch of times.

view this post on Zulip Simon Hudon (Mar 04 2020 at 21:23):

Maybe that's a better solution then

view this post on Zulip Simon Hudon (Mar 04 2020 at 21:56):

making things protected seem to fix the issue

view this post on Zulip Simon Hudon (Mar 04 2020 at 22:05):

https://github.com/leanprover-community/lean/pull/138


Last updated: May 06 2021 at 22:13 UTC