Zulip Chat Archive

Stream: general

Topic: tidy lost my metavars


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 29 2018 at 10:08):

the recover tactic does this, essentially

view this post on Zulip Johan Commelin (Nov 29 2018 at 10:12):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Keeley Hoek (Nov 29 2018 at 13:40):

Seems like a bug in constructor to me

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 29 2018 at 13:42):

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

view this post on Zulip Keeley Hoek (Nov 29 2018 at 13:43):

I'm not sure I understand

view this post on Zulip Keeley Hoek (Nov 29 2018 at 13:43):

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

view this post on Zulip Johan Commelin (Nov 29 2018 at 13:43):

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

view this post on Zulip 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

view this post on Zulip Keeley Hoek (Nov 29 2018 at 13:45):

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

view this post on Zulip Johan Commelin (Nov 29 2018 at 13:48):

Thanks for debugging this!


Last updated: May 08 2021 at 18:17 UTC