## Stream: general

### Topic: tidy lost my metavars

#### Johan Commelin (Nov 29 2018 at 09:29):

Somehow tidy claims it closed all goals, but the kernel says there are still metavariables left. Is there a good approach to debugging this? Somewhere a metavariable got removed from the goal-list without being fully instantiated. I guess it should be possible to track this, right?

#### Mario Carneiro (Nov 29 2018 at 10:07):

it is possible to write a tactic that will tell you if the current tactic state is broken, but you will have to sprinkle it around and it will often give false positives because of focus and such

#### Mario Carneiro (Nov 29 2018 at 10:08):

the recover tactic does this, essentially

#### Johan Commelin (Nov 29 2018 at 10:12):

Thanks. Didn't know about recover. I'll try it out.

#### Johan Commelin (Nov 29 2018 at 12:06):

Oh by the way, recover worked. It figured out that there was some naturality condition that wasn't proven. I don't know how it got lost.

#### Keeley Hoek (Nov 29 2018 at 12:11):

It'd be really great to see a reproducible case of that Johan, probably there is a bug in a tactic somewhere

#### Johan Commelin (Nov 29 2018 at 12:26):

@Keeley Hoek https://github.com/leanprover-community/mathlib/blob/sheaf/category_theory/presheaf.lean#L113
Voila. I retried this with a freshly restarted Lean. Problem still occurs. I have no idea how I could build a MWE out of this. It's pretty deep down in ugly maths.

#### Keeley Hoek (Nov 29 2018 at 13:40):

Seems like a bug in constructor to me

#### Keeley Hoek (Nov 29 2018 at 13:41):

For anyone who is interested:

def oopsie (F : C ⥤ D) : functor.id (presheaf C) ⟹ yoneda_extension F ⋙ restricted_yoneda F :=
begin
constructor,
-- One goal
recover,
-- Two goals :O
sorry
end


#### Johan Commelin (Nov 29 2018 at 13:42):

But I guess this ties in to the auto_params, doesn't it?

#### Keeley Hoek (Nov 29 2018 at 13:43):

I'm not sure I understand

#### Keeley Hoek (Nov 29 2018 at 13:43):

I mean, surely it shouldn't erase a metavar it creates from history

#### Johan Commelin (Nov 29 2018 at 13:43):

Maybe constructor is throwing away goals that have an auto_param attached to them?

#### Keeley Hoek (Nov 29 2018 at 13:45):

I wonder if the extract_opt_auto_param in get_constructors_for has anything to do with it
Actually, I bet it is the mk_const on line 23 of constructor_tactic.lean in lean core

#### Keeley Hoek (Nov 29 2018 at 13:45):

That could create metavariables which don't get fully bound by the apply maybe

#### Johan Commelin (Nov 29 2018 at 13:48):

Thanks for debugging this!

Last updated: May 08 2021 at 18:17 UTC