Zulip Chat Archive

Stream: general

Topic: conv in lean master


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

view this post on Zulip Yury G. Kudryashov (Oct 23 2020 at 20:02):

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

view this post on Zulip Eric Wieser (Oct 23 2020 at 20:02):

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

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

view this post on Zulip Yury G. Kudryashov (Oct 23 2020 at 20:03):

Have you tried building mathlib with lean master?

view this post on Zulip Eric Wieser (Oct 23 2020 at 20:04):

No

view this post on Zulip Eric Wieser (Oct 23 2020 at 20:04):

Can you point me to a failed build log?

view this post on Zulip Eric Wieser (Oct 23 2020 at 20:05):

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

view this post on Zulip Yury G. Kudryashov (Oct 23 2020 at 20:06):

One of failing convs is in src#cardinal.prod_ne_zero

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

view this post on Zulip Yury G. Kudryashov (Oct 23 2020 at 20:10):

Can you just try to build mathlib with lean master?

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

view this post on Zulip Eric Wieser (Oct 23 2020 at 20:12):

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

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

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

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

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

view this post on Zulip Eric Wieser (Oct 23 2020 at 20:28):

Self-contained #mwe in released lean:

view this post on Zulip Yury G. Kudryashov (Oct 23 2020 at 20:32):

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

view this post on Zulip Eric Wieser (Oct 23 2020 at 20:32):

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

view this post on Zulip Yury G. Kudryashov (Oct 23 2020 at 20:33):

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

view this post on Zulip Eric Wieser (Oct 23 2020 at 20:34):

Not yet, but trying to

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

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

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

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

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

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

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

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

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