tactic state: vm check failed

Stream: general

[Eric Rodriguez]

consider this mwe:

import data.finset.basic

variables {α : Type*} (x y : finset α)

include x y

noncomputable def my_union :=
have _ := classical.dec_eq α, by exactI x ∪ y

lemma asd [decidable_eq α] : my_union x y = x ∪ y :=
begin
  rw my_union,
  convert rfl
end

#print asd

trying to view the tactic state, you get a weird error, but the proof seems to compile (I haven't checked it with trepplein or anything yet.

image.png

[Gabriel Ebner]

Does this look like https://github.com/leanprover-community/lean/issues/673 ?

[Eric Rodriguez]

yep, precisely like it

[Eric Rodriguez]

although the mwes look fairly different, and there's no sorry like in Mario's example

[Kevin Buzzard]

oh man, you were going to get a point for that (new error that nobody saw before), but Mario gets it instead

[Gabriel Ebner]

Is the workaround of switching to plain text mode acceptable for you? I'm not sure I want to spend time debugging this in Lean 3.

[Mario Carneiro]

the sorry is so that it works without mathlib

[Mario Carneiro]

I like your MWE better than mine though, since it doesn't involve well founded recursion

[Eric Rodriguez]

oh it's fine, just thought I would post it; I'm happy there was a workaround! this doesn't happen if you simp only the term, though, which is worth knowing

[Mario Carneiro]

Minimized as far as possible within lean:

open tactic tagged_format
#eval do
  --                                vvvvv-- zoom in to this subexpr
  e ← tactic.to_expr ``(have this : sorry, from sorry, true),
  ts ← tactic.read,
  compose (group $ compose (group $ compose _have_this $ compose _colon m) _sorry) _true
    ← pure (tactic_state.pp_tagged ts e),
  nest _ (compose (compose (compose (compose _nl m) _comma) _space) _from_sorry) ← pure m,
  tag ([coord], _sorry_expr) _sorry ← pure m,
  tactic.trace e,
  -- case on coord causes VM bug
  match coord with
  | expr.coord.app_arg := pure ()
  | _ := pure ()
  end

[Mario Carneiro]

that is, it appears tactic_state.pp_tagged does not know how to express the subexpression coordinate corresponding to the type of a have or suffices expression

[Mario Carneiro]

It also seems pretty sketchy that the lean inductive expr.coord has 9 constructors but the corresponding C++ type has 11 constructors, with the two extra being mvar_type, local_const_type which sound like they shouldn't be escaping but should probably exist in the lean type anyway

[Mario Carneiro]

Turns out the only use of those constructors was in pp output for have statements, so... I just removed them and it worked

[Mario Carneiro]

lean#682

[Yaël Dillies]

Always nice when the fix is to delete code.

[Mario Carneiro]

TIL that suffices doesn't actually leave any trace in the term, unlike have, so when you print it back you get a lambda

[Mario Carneiro]

I was looking for a pp_suffices in the code but there isn't any

[Mario Carneiro]

#check have x : true, from trivial, trivial
-- have x : true, from trivial, trivial : true

#check suffices x : true, from trivial, trivial
-- (λ (x : true), trivial) trivial : true

[Alex J. Best]

I remember there being some trace in the term before, it's how i implemented https://github.com/leanprover-community/mathlib/blob/8c60a9270b26c63b1492845d39cd8258418fa64a/src/tactic/lint/misc.lean#L407 did that now change, or is it just not printed?

[Mario Carneiro]

hm, you are not wrong... it looks like there is an annotation but it is in a different place than have

#eval do
  e ← tactic.to_expr ``(have x:bool, from bool.ff, bool.tt),
  tactic.trace e.to_raw_fmt
-- (app [macro annotation (lam x default (const bool []) [macro annotation (const bool.tt [])])] (const bool.ff []))
#eval do
  e ← tactic.to_expr ``(suffices x:bool, from bool.ff, bool.tt),
  tactic.trace e.to_raw_fmt
-- [macro annotation (app (lam x default (const bool []) (const bool.ff [])) (const bool.tt []))]