Zulip Chat Archive

Stream: general

Topic: trolled by undergrad


view this post on Zulip Kevin Buzzard (Jul 20 2018 at 18:34):

It took me 20 minutes to diagnose this deterministic time-out:

import analysis.real

theorem infinite_cover {a b : } {c : set (set )} (n : ) :
 k : , 1  k  n   c'  c, {r :  | a+(k-1)*(a+b)/n  r  r  a+k*(a+b)/n}  ⋃₀ c'  ¬ set.finite c' := sorry

In my defence, the code was far longer to begin with, and probably about 15 were spent reducing it to this.

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 18:48):

I'm about to set off for home and I'll spill the beans if nobody has spotted it by the time I get in

view this post on Zulip Patrick Massot (Jul 20 2018 at 18:49):

I don't understand what you are asking for

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 18:50):

Cut and paste that code -- it times out

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 18:50):

deterministic time-out

view this post on Zulip Chris Hughes (Jul 20 2018 at 18:50):

1 ≤ k ≤ n

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 18:50):

:-)

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 18:50):

I spotted it when I changed n to 1

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 18:51):

I was quite surprised that the statement managed to parse

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 18:51):

in retrospect

view this post on Zulip Mario Carneiro (Jul 20 2018 at 18:52):

because obviously k ≤ n is also a nat

view this post on Zulip Mario Carneiro (Jul 20 2018 at 18:52):

bigger than one no less

view this post on Zulip Chris Hughes (Jul 20 2018 at 18:52):

is left or right associative?

view this post on Zulip Mario Carneiro (Jul 20 2018 at 19:01):

left assoc, my bad

view this post on Zulip Mario Carneiro (Jul 20 2018 at 19:02):

infix ≤        := has_le.le

infix means infixl

view this post on Zulip Mario Carneiro (Jul 20 2018 at 19:02):

oh I see so it tried to find a Prop coercion for n

view this post on Zulip Mario Carneiro (Jul 20 2018 at 19:03):

and then it means "if 1 <= k then n"

view this post on Zulip Mario Carneiro (Jul 20 2018 at 19:04):

1 ≤ k ≤ (n ≤ 1) parses just fine

view this post on Zulip Chris Hughes (Jul 20 2018 at 19:04):

Because Prop has an order structure for some reason.

view this post on Zulip Mario Carneiro (Jul 20 2018 at 19:04):

because Prop has a natural order structure...

view this post on Zulip Mario Carneiro (Jul 20 2018 at 19:05):

which we use funky notation for

view this post on Zulip Mario Carneiro (Jul 20 2018 at 19:06):

In fact I'm pretty sure boolean algebras are basically generalized Prop

view this post on Zulip Mario Carneiro (Jul 21 2018 at 02:17):

@Sebastian Ullrich I just noticed that this error is a bit subtler than expected. It doesn't give a instance overflow error, it times out and produces no output in the trace. Do you know how the typeclass instance mechanism could run out of time without overflowing?

view this post on Zulip Mario Carneiro (Jul 21 2018 at 02:19):

example without trolling:

import analysis.real
example (n : ℕ) : Prop := n

view this post on Zulip Mario Carneiro (Jul 21 2018 at 02:45):

Ah, I finally got an instance trace, and it does something I didn't think the typeclass inference engine does: it repeatedly does the same search, at the same depth level, which is why it timeouts from iteration rather than recursion. Here's the beginning, with the depth shown using indentation:

(0) ?x_3 : has_coe_to_sort ℕ := @coe_sort_trans ?x_5 ?x_6 ?x_7 ?x_8
 (1) ?x_7 : has_coe_t_aux ℕ ?x_6 := @coe_base_aux ?x_9 ?x_10 ?x_11
  (2) ?x_11 : has_coe ℕ ?x_10 := int.has_coe
 (1) ?x_8 : has_coe_to_sort ℤ := @coe_sort_trans ?x_22 ?x_23 ?x_24 ?x_25
  (2) ?x_24 : has_coe_t_aux ℤ ?x_23 := @coe_base_aux ?x_26 ?x_27 ?x_28
   (3) ?x_28 : has_coe ℤ ?x_27 := @int.cast_coe ?x_49 ?x_50 ?x_51 ?x_52 ?x_53
    (4) ?x_50 : has_zero ?x_49 := real.has_zero
    (4) ?x_51 : has_one ℝ := real.has_one
    (4) ?x_52 : has_add ℝ := real.has_add
    (4) ?x_53 : has_neg ℝ := real.has_neg
  (2) ?x_25 : has_coe_to_sort ℝ := @coe_sort_trans ?x_55 ?x_56 ?x_57 ?x_58
   (3) ?x_57 : has_coe_t_aux ℝ ?x_56 := @coe_base_aux ?x_59 ?x_60 ?x_61
   (3) ?x_57 : has_coe_t_aux ℝ ?x_56 := @coe_trans_aux ?x_59 ?x_60 ?x_61 ?x_62 ?x_63
    (4) ?x_53 : has_neg ℝ := @lattice.boolean_algebra.to_has_neg ?x_60 ?x_61
     (5) ?x_61 : lattice.boolean_algebra ℝ := @lattice.complete_boolean_algebra.to_boolean_algebra ?x_62 ?x_63
    (4) ?x_53 : has_neg ℝ := @add_group.to_has_neg ?x_55 ?x_56
     (5) ?x_56 : add_group ℝ := real.add_group
  (2) ?x_25 : has_coe_to_sort ℝ := @coe_sort_trans ?x_58 ?x_59 ?x_60 ?x_61
   (3) ?x_60 : has_coe_t_aux ℝ ?x_59 := @coe_base_aux ?x_62 ?x_63 ?x_64
   (3) ?x_60 : has_coe_t_aux ℝ ?x_59 := @coe_trans_aux ?x_62 ?x_63 ?x_64 ?x_65 ?x_66
     (5) ?x_56 : add_group ℝ := @add_comm_group.to_add_group ?x_59 ?x_60
      (6) ?x_60 : add_comm_group ℝ := real.add_comm_group
  (2) ?x_25 : has_coe_to_sort ℝ := @coe_sort_trans ?x_62 ?x_63 ?x_64 ?x_65
   (3) ?x_64 : has_coe_t_aux ℝ ?x_63 := @coe_base_aux ?x_66 ?x_67 ?x_68
   (3) ?x_64 : has_coe_t_aux ℝ ?x_63 := @coe_trans_aux ?x_66 ?x_67 ?x_68 ?x_69 ?x_70
      (6) ?x_60 : add_comm_group ℝ := @nonneg_comm_group.to_add_comm_group ?x_61 ?x_62
       (7) ?x_62 : nonneg_comm_group ℝ := @linear_nonneg_ring.to_nonneg_comm_group ?x_63 ?x_64
       (7) ?x_62 : nonneg_comm_group ℝ := @nonneg_ring.to_nonneg_comm_group ?x_63 ?x_64
        (8) ?x_64 : nonneg_ring ℝ := @linear_nonneg_ring.to_nonneg_ring ?x_65 ?x_66
      (6) ?x_60 : add_comm_group ℝ := @ring.to_add_comm_group ?x_63 ?x_64
       (7) ?x_64 : ring ℝ := real.ring
  (2) ?x_25 : has_coe_to_sort ℝ := @coe_sort_trans ?x_66 ?x_67 ?x_68 ?x_69
   (3) ?x_68 : has_coe_t_aux ℝ ?x_67 := @coe_base_aux ?x_70 ?x_71 ?x_72
   (3) ?x_68 : has_coe_t_aux ℝ ?x_67 := @coe_trans_aux ?x_70 ?x_71 ?x_72 ?x_73 ?x_74
       (7) ?x_64 : ring ℝ := @nonneg_ring.to_ring ?x_71 ?x_72
        (8) ?x_72 : nonneg_ring ℝ := @linear_nonneg_ring.to_nonneg_ring ?x_73 ?x_74
       (7) ?x_64 : ring ℝ := @domain.to_ring ?x_65 ?x_66
        (8) ?x_66 : domain ℝ := real.domain

view this post on Zulip Mario Carneiro (Jul 21 2018 at 02:45):

notice that (2) ?x_25 : has_coe_to_sort ℝ keeps coming up; this continues for all 38000 lines of output before it times out

view this post on Zulip Mario Carneiro (Jul 21 2018 at 03:24):

Oh whoa I just figured out why this is happening, and why it's called a "prolog-like search" - nota bene @Kevin Buzzard :)

Whenever it tries something which doesn't work, it reverts all the metavariable assignments up to that point and then tries again. Like here around the newline:

  (2) ?x_25 : has_coe_to_sort ℝ := @coe_sort_trans ?x_55 ?x_56 ?x_57 ?x_58
   (3) ?x_57 : has_coe_t_aux ℝ ?x_56 := @coe_base_aux ?x_59 ?x_60 ?x_61
   (3) ?x_57 : has_coe_t_aux ℝ ?x_56 := @coe_trans_aux ?x_59 ?x_60 ?x_61 ?x_62 ?x_63
    (4) ?x_53 : has_neg ℝ := @lattice.boolean_algebra.to_has_neg ?x_60 ?x_61
     (5) ?x_61 : lattice.boolean_algebra ℝ := @lattice.complete_boolean_algebra.to_boolean_algebra ?x_62 ?x_63
    (4) ?x_53 : has_neg ℝ := @add_group.to_has_neg ?x_55 ?x_56
     (5) ?x_56 : add_group ℝ := real.add_group

  (2) ?x_25 : has_coe_to_sort ℝ := @coe_sort_trans ?x_58 ?x_59 ?x_60 ?x_61
   (3) ?x_60 : has_coe_t_aux ℝ ?x_59 := @coe_base_aux ?x_62 ?x_63 ?x_64
   (3) ?x_60 : has_coe_t_aux ℝ ?x_59 := @coe_trans_aux ?x_62 ?x_63 ?x_64 ?x_65 ?x_66
     (5) ?x_56 : add_group ℝ := @add_comm_group.to_add_group ?x_59 ?x_60
      (6) ?x_60 : add_comm_group ℝ := real.add_comm_group

The line (5) ?x_56 : add_group ℝ := real.add_group is a failure, but it assigns a value to ?x_56 from the (2) line. So it rolls all the way back to the (2) line and replays the same assignments until it gets to the bad choice real.add_group, and tries something different, in this case @add_comm_group.to_add_group ?x_59 ?x_60.

view this post on Zulip Mario Carneiro (Jul 21 2018 at 03:28):

I wonder if typeclass search will change in lean 4. This seems like such a poor strategy I'm surprised it works as well as it does in mathlib. I know Leo thinks many things about lean 3 are fundamentally broken, and I wouldn't be surprised if this was on the list

view this post on Zulip Sebastian Ullrich (Jul 21 2018 at 08:21):

@Mario Carneiro This is not how class inference should work, nor have I seen such a trace before. Class inference uses temporary mvars that can be unassigned individually. https://github.com/leanprover/lean/blob/ceacfa7445953cbc8860ddabc55407430a9ca5c3/src/library/type_context.cpp#L1405

view this post on Zulip Mario Carneiro (Jul 21 2018 at 08:23):

If you like I can make a mathlib-free example

view this post on Zulip Sebastian Ullrich (Jul 21 2018 at 08:26):

That would be great, thanks

view this post on Zulip Mario Carneiro (Jul 21 2018 at 08:39):

I think this should do the trick (WARNING: this brings VSCode to its knees due to quantity of output)

@[priority 0] instance cast_coe {α} [has_zero α] [has_one α] [has_add α] : has_coe ℕ α := ⟨λ _, 0⟩
constant R : Type
instance : has_zero R := sorry

set_option trace.class_instances true
example (n : ℕ) : Prop := n

The constant R is optional but gives the typeclass system something to fixate on rather than whatever random thing it finds first (usually unsigned for me on the init library and real when it is imported)

view this post on Zulip Sebastian Ullrich (Jul 21 2018 at 08:42):

hmm

$ lean +3.4.1 scratch.lean |& wc -l
381659
 $ lean +master scratch.lean |& wc -l
3342

I guess Leo fixed it already :D

view this post on Zulip Mario Carneiro (Jul 21 2018 at 08:45):

well... I'm glad it was fixed, although I'm still puzzled over the cause...

view this post on Zulip Mario Carneiro (Jul 21 2018 at 08:59):

Oh, looking at the trace from that version, I noticed that it searches for (1) ?x_7 : has_coe_to_sort ℤ 2826 times (with 26000 lines in between, not counting failures) before finally getting to (1) ?x_7 : has_coe_to_sort ℕ, which is the same typeclass search it started with. So I think if I let it run long enough it would hit the recursion limit, it would just take an extremely long time to do so.

view this post on Zulip Patrick Massot (Jul 21 2018 at 09:00):

Maybe it would be worth checking that it was not fixed by accident (since another modification could reinstate the bug), or at least add it to the test suite?

view this post on Zulip Patrick Massot (Jul 21 2018 at 09:02):

Do you think the type class search could become more programmable for users? For instance we already saw that it would be nice to be able to tell it: whenever you're looking for ring ?x_i then you should give up on that branch.

view this post on Zulip Mario Carneiro (Jul 21 2018 at 09:02):

I'm not sure how much I should care about this bug, since it has to do with lean performance on an unsuccessful typeclass search anyway

view this post on Zulip Mario Carneiro (Jul 21 2018 at 09:03):

I think "negative instances" would be great, they could probably speed up the search a lot. I.e. unsigned is not a field, stop looking there

view this post on Zulip Patrick Massot (Jul 21 2018 at 09:03):

Obviously I don't know either, this is far above my competences. My reaction is only triggered by Sebastian not knowing something has been fixed

view this post on Zulip Mario Carneiro (Jul 21 2018 at 09:04):

but there is a lot of planning necessary to get a feature like that right

view this post on Zulip Mario Carneiro (Jul 21 2018 at 09:04):

and obviously it's up to Sebastian and Leo to make that happen

view this post on Zulip Mario Carneiro (Jul 21 2018 at 09:05):

so I will just let them ponder and figure out whatever works

view this post on Zulip Patrick Massot (Jul 21 2018 at 09:05):

and soon Gabriel, according to Leo's talk

view this post on Zulip Sebastian Ullrich (Jul 21 2018 at 09:05):

The type context will remain in C++, so it will not be arbitrarily configurable like other parts (hopefully will)

view this post on Zulip Mario Carneiro (Jul 21 2018 at 09:06):

is typeclass search done in the type context?

view this post on Zulip Patrick Massot (Jul 21 2018 at 09:06):

You could still let users pass options to the C++ code, couldn't you?

view this post on Zulip Sebastian Ullrich (Jul 22 2018 at 15:30):

@Mario Carneiro Yes, it uses many type context internals. Still, reimplementing it on top of the new type context monad may be an interesting idea, now that I think about it.

view this post on Zulip Sebastian Ullrich (Jul 22 2018 at 15:31):

@Patrick Massot Sure, that's what I meant by "not arbitrarily". For the parts reimplemented in Lean, I'd like users to be able to completely replace the default implementations if they want to.

view this post on Zulip Mario Carneiro (Jul 22 2018 at 15:32):

it would certainly be good if at least potential writing of the typeclass search could guide what of the type context gets exposed to lean

view this post on Zulip Sebastian Ullrich (Jul 22 2018 at 15:32):

Yes, exactly


Last updated: May 18 2021 at 17:44 UTC