conv in lean master

Stream: general

[Yury G. Kudryashov]

I'm building mathlib with lean from the branch dropDLO, and I get some failures that seem completely unrelated to decidable_linear_order: some conv in ... expressions now fail to match.

[Yury G. Kudryashov]

With error like error: find converter failed, pattern was not found

[Eric Wieser]

This sounds like a change I made to the conv find command

[Eric Wieser]

Although if anything my changes should have resulted in that error message being replaced with a more useful one

[Yury G. Kudryashov]

Have you tried building mathlib with lean master?

[Eric Wieser]

No

[Eric Wieser]

Can you point me to a failed build log?

[Eric Wieser]

(this is the change I'm referring to: https://github.com/leanprover-community/lean/commit/adb4258b6a287d445237165811a967e6ab7c0327)

[Yury G. Kudryashov]

One of failing convs is in src#cardinal.prod_ne_zero

[Eric Wieser]

I'm not sure how to easily get in a position to experiment - does replacing that line with conv { find (f _) {rw ← mk_out (f i) } } produce a better error? Perhaps src#tactic.interactive.conv is hiding the real error...

[Yury G. Kudryashov]

Can you just try to build mathlib with lean master?

[Yury G. Kudryashov]

445:10: find converter failed, pattern was not found
state:
ι : Type u_1,
f : ι → cardinal
⊢ (prod f ≠ 0 ↔ ∀ (i : ι), f i ≠ 0) = ?m_1

[Eric Wieser]

I have no idea how to actually do that...

[Eric Wieser]

If you're getting this from a CI build, can I do the equivalent of a get-cache to avoid needing to build it myself?

[Yury G. Kudryashov]

@Gabriel Ebner We should add it to some docs, and add a link to these docs from lean PR template.

1. Build lean master using cmake.
2. Install it to some directory.
3. Run elan toolchain link my-name PATH.
4. Put my-name into leanpkg.toml

[Reid Barton]

You can even skip step 2, and replace 4 by using elan override, for a one-off thing

[Eric Wieser]

In this case, I'll see if I can reproduce the issue with a copy of the new find in old lean

[Eric Wieser]

Self-contained #mwe in released lean:

import tactic
import init.meta.interactive
import init.meta.converter.conv
import set_theory.cardinal

namespace tactic

open tactic_result

variables {α : Type}

meta def capture (t : tactic α) : tactic (tactic_result α) :=
λ s, match t s with
| (success r s') := success (success r s') s'
| (exception f p s') := success (exception f p s') s'
end

meta def resume {α : Type*} (t : tactic_result α) : tactic α :=
λ s, t

end tactic

namespace conv
namespace interactive

open lean
open lean.parser
open interactive
open interactive.types
open tactic_result

meta def find2 (p : parse parser.pexpr) (c : itactic) : conv unit :=
do (r, lhs, _) ← tactic.target_lhs_rhs,
   pat ← tactic.pexpr_to_pattern p,
   s   ← simp_lemmas.mk_default, -- to be able to use congruence lemmas @[congr]
   -- we have to thread the tactic state through `ext_simplify_core` manually
   st ← tactic.read,
   (found_result, new_lhs, pr) ← tactic.ext_simplify_core
     (success ff st)  -- loop counter
     {zeta := ff, beta := ff, single_pass := tt, eta := ff, proj := ff,
      fail_if_unchanged := ff, memoize := ff}
     s
     (λ u, return u)
     (λ found_result s r p e, do
       found ← tactic.resume found_result,
       guard (not found),
       matched ← (tactic.match_pattern pat e >> return tt) <|> return ff,
       guard matched,
       res ← tactic.capture (c.convert e r),
       -- If an error occurs in conversion, capture it; `ext_simplify_core` will not
       -- propagate it.
       match res with
       | (success r s')     := return (success tt s',    r.fst, some r.snd, ff)
       | (exception f p s') := return (exception f p s', e,     none,       ff)
       end)
     (λ a s r p e, tactic.failed)
     r lhs,
  found ← tactic.resume found_result,
  when (not found) $ tactic.fail "find converter failed, pattern was not found",
  update_lhs new_lhs pr

end interactive
end conv

theorem prod_ne_zero2 {ι} (f : ι → ℕ) : true ↔ ∀ i, f i ≠ 0 :=
begin
  conv {
    find2 (f _) {  -- find works
      -- rw ← mk_out (f i)
    },
  },
  sorry
end

[Yury G. Kudryashov]

Does it work (I don't want to switch to another branch right now)?

[Eric Wieser]

No, I get the same problem (but you can run that in the web editor)

[Yury G. Kudryashov]

Do you understand why it fails and the old find works?

[Eric Wieser]

Not yet, but trying to

[Eric Wieser]

How can I trace a pattern object? tactic.trace format!"Pattern was: {pat}" fails, but it works for {e}

[Yury G. Kudryashov]

In the meantime I'm golfing all proofs that fail because of this bug, and IMO they look better without conv in.

[Eric Wieser]

I mean, that was sort of the opposite of the intent of that patch, but oh well. If using the new lean is urgent, then I guess we can revert the patch - otherwise, I'll keep trying to understand what's going on

[Yury G. Kudryashov]

We can definitely wait for a day or two. And we can decide whether to revert (some of) my changes once you fix find.

[Eric Wieser]

The error seems to be accurate - tactic.match_pattern pat e really is failing when pat is pattern.mk (f ?x_0) [] [] 0 1 and e is f _

[Eric Wieser]

It looks like it was the change suggested by @Gabriel Ebner in that PR to propagate both the error and success states that broke things

[Eric Wieser]

If I replace both calls to tactic.resume with tactic.unpack, then your example passes (but the tests added in that PR fail)

[Eric Wieser]

My hunch is that the C++ is caching metavariables outside of the tactic state, meaning that it gets confused when the lean callback adjusts the tactic state on it.

[Eric Wieser]

PR is merged, the regression should be fixed now