tidy lost my metavars

Stream: general

[Johan Commelin]

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]

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]

the recover tactic does this, essentially

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Johan Commelin]

@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]

Seems like a bug in constructor to me

[Keeley Hoek]

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]

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

[Keeley Hoek]

I'm not sure I understand

[Keeley Hoek]

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

[Johan Commelin]

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

[Keeley Hoek]

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]

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

[Johan Commelin]

Thanks for debugging this!