## Stream: general

### Topic: conv in lean master

#### Yury G. Kudryashov (Oct 23 2020 at 20:02):

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 (Oct 23 2020 at 20:02):

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

#### Eric Wieser (Oct 23 2020 at 20:02):

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

#### Eric Wieser (Oct 23 2020 at 20:03):

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

#### Yury G. Kudryashov (Oct 23 2020 at 20:03):

Have you tried building mathlib with lean master?

No

#### Eric Wieser (Oct 23 2020 at 20:04):

Can you point me to a failed build log?

#### Eric Wieser (Oct 23 2020 at 20:05):

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

#### Yury G. Kudryashov (Oct 23 2020 at 20:06):

One of failing convs is in src#cardinal.prod_ne_zero

#### Eric Wieser (Oct 23 2020 at 20:08):

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 (Oct 23 2020 at 20:10):

Can you just try to build mathlib with lean master?

#### Yury G. Kudryashov (Oct 23 2020 at 20:10):

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 (Oct 23 2020 at 20:12):

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

#### Eric Wieser (Oct 23 2020 at 20:17):

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 (Oct 23 2020 at 20:17):

@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 (Oct 23 2020 at 20:18):

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

#### Eric Wieser (Oct 23 2020 at 20:21):

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

#### Eric Wieser (Oct 23 2020 at 20:28):

Self-contained #mwe in released lean:

#### Yury G. Kudryashov (Oct 23 2020 at 20:32):

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

#### Eric Wieser (Oct 23 2020 at 20:32):

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

#### Yury G. Kudryashov (Oct 23 2020 at 20:33):

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

#### Eric Wieser (Oct 23 2020 at 20:34):

Not yet, but trying to

#### Eric Wieser (Oct 23 2020 at 20:35):

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

#### Yury G. Kudryashov (Oct 23 2020 at 20:41):

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

#### Eric Wieser (Oct 23 2020 at 20:42):

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 (Oct 23 2020 at 20:45):

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 (Oct 23 2020 at 20:56):

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 (Oct 23 2020 at 21:05):

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 (Oct 23 2020 at 21:06):

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 (Oct 23 2020 at 21:16):

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 (Oct 26 2020 at 10:51):

PR is merged, the regression should be fixed now

Last updated: May 12 2021 at 23:13 UTC