deterministic time-out

Stream: general

[Kevin Buzzard]

What can cause a deterministic time-out? Can I read anything into the red squiggles to help me find out where it is?

timeout.png

[Kevin Buzzard]

That code has three errors. They are all "deterministic time-out". I am trying to define a term of a given type. I have begun to fully elaborate everything in an attempt to find out where the problem is.

[Kevin Buzzard]

But I don't know what is causing the time-out. How can I debug this?

[Kevin Buzzard]

timeout2.png

[Kevin Buzzard]

I have now fully elaborated all of the terms with red underlines and I don't know what to do next.

[Kevin Buzzard]

timeout3.png

[Kevin Buzzard]

What causes timeouts in Lean?

[Kevin Buzzard]

@Mario Carneiro help!

[Mario Carneiro]

You can use by try_for 1000 {exact bla} in place of bla

[Kevin Buzzard]

Thanks

[Kevin Buzzard]

I'm visiting Johan in Freiburg at the minute and today is my last day

[Kevin Buzzard]

so we're in a bit of a rush ;-)

[Mario Carneiro]

that will allow you to control where the timeout happens, play with surrounding bits of your code with it

[Mario Carneiro]

also you can incrementally build the term using refine

[Kevin Buzzard]

unknown identifier exact

[Kevin Buzzard]

What is a thunk?

[Mario Carneiro]

do you have mathlib tactics?

[Mario Carneiro]

try_for is also a pure function, that's not what you want

[Mario Carneiro]

there is a try_for tactic in mathlib

[Kevin Buzzard]

timeout4.png

[Mario Carneiro]

a thunk A is the same as unit -> A, as you can see from the definition, but the lambda unit can be omitted by parser magic

[Mario Carneiro]

by

[Kevin Buzzard]

try_for timeout, using sorry

[Mario Carneiro]

increase the number if it's too timeout happy

[Kevin Buzzard]

That's using the tactic

[Kevin Buzzard]

I tried 10000

[Mario Carneiro]

right, that's the expected result

[Kevin Buzzard]

Fails on 100000

[Mario Carneiro]

but now you can break up your term into bits, and elaborate it all separately to find the hotspot

[Kevin Buzzard]

I thought I already did this with the @ stuff

[Kevin Buzzard]

I just get "timeout". Can you look at the red squiggles? Are they any indication of where the problem is?

[Mario Carneiro]

i.e. instead of

begin
  try_for 1000 { exact foo bar baz }
end

try

begin
  try_for 1000 { refine foo _ _ },
  try_for 1000 { exact bar },
  try_for 1000 { exact baz }
end

[Mario Carneiro]

try to figure out what part of the elaboration is taking all the time

[Mario Carneiro]

I don't know how trustworthy the red squiggle locations are for timeouts

[Kevin Buzzard]

OK many thanks for these tips. I'll try to take it from here.

[Kevin Buzzard]

Mario -- many thanks indeed. These ideas are exactly the tool I need to debug this very frustrating issue.

[Kevin Buzzard]

OK wonderful -- I have got to the heart of things!

I have X : Type and then def Y (v : random_parameter) := X, so X and Y v are defeq. I now have uniform space structures on X and Y, and I think of them as defeq too, but Lean does not even understand what that assertion means because they are terms of different types.

OK so the actual thing I want is the following: I have a multiplication defined on ring_completion X and a multiplication defined on ring_completion (Y v) and the multiplications are defined using some continuous extension of a topology coming from the uniform space structures which I think of as defeq but which are not because this doesn't make sense. I think of these multiplications as defeq. But they are not. And Lean is struggling to prove that the map which I would call the identity map is a monoid homomorphism, because to identify the multiplications it needs to identify the structures all the way down.

@Mario Carneiro this is another instance of missing transfer functionality, isn't it? I can give you an equiv f:X -> Y and now I want an equiv u(f): uniform_space X -> uniform_space Yand t(f): topological_ring X -> topological_ring Y and then I want an equiv topological_ring (@ring_completion uX tX X) -> topological_ring (@ring_completion (u(f) uX) (t(f) tX) Y). Am I making sense here? In our case X -> Y is id but even in this case we're having problems. Should we be? Perhaps we have made an actual maths error under the hood somewhere and our ring structures are really "what I would call defeq".

equal are multiplications defined using the topological structures coming from the ring completions which use these uniform structures

[Mario Carneiro]

From your description of X and Y v, they should actually be defeq, and you can take typeclass arguments from one and use it for the other. But because Y is not a reducible def, it will affect typeclass inference, i.e. it will probably find different instances, and those instances might not be defeq to the ones you get with X

[Kevin Buzzard]

Yes, I think my underlying problem must be a mathematical one