deterministic timeout

Stream: new members

[Michael Beeson]

I sometimes but not always get errors like
inf.lean:153:0: error
(deterministic) timeout

The line is always the start of a new lemma. #check commands
show that the previous lemmas were indeed proved and the
next lemma was indeed proved. Should I worry about this error?
What causes it?

[Reid Barton]

Something tried to run for too long and Lean gave up on that particular lemma.

[Michael Beeson]

Well, but it didn't give up because all the lemmas are actually proved.

[Reid Barton]

You said the previous and next lemmas were proved, not the current lemma.

[Reid Barton]

But also #check won't complain if the lemma wasn't actually proved. Basically it's as though you wrote lemma ... := sorry, I think.

[Michael Beeson]

All the lemmas in the whole file are correctly proved. The error mentions a line number that is the
first line of one lemma. By previous and next I meant, the one preceding that line, and the one starting on that line.

[Michael Beeson]

Oh! That is very important thing to know!

[Reid Barton]

If you see any error, like this one, it means your file was not accepted.

[Reid Barton]

You can also use #print axioms lemma_name to test this.

[Reid Barton]

As a technical note, Lean checks proofs of lemmas in parallel, with the lemma statement added to the environment immediately on the main task--so when Lean gets to #check, it doesn't necessarily even know yet whether or not the lemma contained an error. But mainly, it would be quite annoying if an error in one lemma prevented any future use of that lemma (imagine you update mathlib and it changes the name of something you use in one place--you want to get one error and not have that cause zillions of downstream errors).

[Michael Beeson]

In the tactic state shown below, if I do exact h201.right I get (after a wait) "deterministic time out". The file does compile OK.
Also the whole project has slowed to a crawl even after compiling and restarting VScode. (On my laptop--I think it's still running OK on my desktop).

h201: b ∈ FINITE M ∧ ∀ (a : M), a ∈ FINITE M → similar M (USC a) (SSC b) → (∃ (z : M), similar M a (SSC z) ∧ similar M b (USC z) ∧ z ⊆ union (SSC b))
⊢ ∀ (a : M), a ∈ FINITE M → similar M (USC a) (SSC b) → (∃ (z : M), similar M a (SSC z) ∧ similar M b (USC z) ∧ z ⊆ union (SSC b))

And it also times out after

   cases h201 with h202 h203,
    exact h203,

although just before the exact, you see that h203 is exactly the goal.

[Bryan Gin-ge Chen]

Can you try and extract a #MWE ? The following doesn't time out, so there must be something going on in code that you haven't shared:

variables (M : Type) [has_subset M]

example (α β : Type) (b : M) (FINITE : Type → set M) (similar : Type → M → M → Prop)
  (USC : M → M) (SSC : M → M) (union : M → M)
  (h201: b ∈ FINITE M ∧
    ∀ (a : M), a ∈ FINITE M → similar M (USC a) (SSC b) →
    (∃ (z : M), similar M a (SSC z) ∧ similar M b (USC z) ∧ z ⊆ union (SSC b))) :
  ∀ (a : M), a ∈ FINITE M → similar M (USC a) (SSC b) →
    (∃ (z : M), similar M a (SSC z) ∧ similar M b (USC z) ∧ z ⊆ union (SSC b)) :=
by exact h201.right

[Sebastien Gouezel]

What happens if you try convert h203 instead of exact h203?

[Michael Beeson]

convert also produces a timeout. I thought perhaps this proof is "too long" so I extracted two long parts as separate lemmas.
One of those lemmas now times out. (In a different place than the original proof). The project does build, but it takes a long time compiling
that proof. Can I just ignore that timeout in interactive mode and rely on the compiled file? But even if I can I don't like it.
Perhaps I made too many calls to "ifinish" in that proof? This does happen both on laptop and desktop by the way.

I can't think how to make a MWE as this project has ten files each with a couple thousand lines of proofs, and this one
is in the ninth file and God knows what all it depends on.

[Mario Carneiro]

it sounds like you might benefit from some code review

[Michael Beeson]

If anyone would like to look at my code they certainly may, in principle. But I'm happy with it, or at least, I was until an hour ago. Since the code does build, and since the proof is accepted up until the very last step, I don't think the problem is in my code.

[Mario Carneiro]

it's quite possible that you are doing something that is not so efficient, and the number of times you use it is catching up to you

[Michael Beeson]

Yes, it's not only possible, it must be so. And, the only likely candidate is "ifinish".

[Mario Carneiro]

in particular, long proofs are bad style in addition to not being handled well by lean. The mere fact that you have a hypothesis h201 means that your proof is 10 times longer than it should be

[Michael Beeson]

That doesn't mean there are 200 hypothesis. They're not numbered consecutively.

[Mario Carneiro]

oh that's good

[Michael Beeson]

Why are long proofs "bad style"?

[Mario Carneiro]

because they are difficult to follow, cause long interactive delays, and make lean consume a lot of memory

[Mario Carneiro]

plus, the longer a proof is the more likely there will be some factorable subparts of independent interest

[Michael Beeson]

Well, you said, "in addition to not being handled well by Lean", but your last two reasons are "not handled well by lean".

[Mario Carneiro]

well mathlib style is in part driven by the current reality of lean

[Mario Carneiro]

it's not just indentation

[Michael Beeson]

I'm not quite sure what "difficult to follow" means. In my proofs, I start with a written proof with numbered or labeled lines. Then in Lean I construct a proof with a line "have formula76" for example and after that a tactic block proving that line. If you fold up those tactic blocks you
see in Lean a proof that exactly corresponds to the written proof. That's my idea of "good style". But I'm willing to learn from people with more experience at this.

[Kevin Buzzard]

Just to be clear -- if there is a time-out in your code then lean is not verifying it -- verification is failing. You can't ignore it.

[Mario Carneiro]

I think numbering things is a bad way to name anything

[Mario Carneiro]

it should be a last resort only

[Michael Beeson]

When I do leanproject build I do not get a timeout message. So then it is verifying it, right? or not?

[Kevin Buzzard]

Where are you seeing the timeouts? In an editor? Which one? Why not increase the time before it times out?

[Michael Beeson]

Now I am naming my lemmas the same names as they get in the LaTeX source files (not by numbers) but I am still numbering the formulas that are numbered in latex.

[Michael Beeson]

I am using VSCode. How can I increase the time?

[Mario Carneiro]

set_option timeout 1000000000000

[Michael Beeson]

I put that command right in my Lean file?

[Mario Carneiro]

between declarations

[Kevin Buzzard]

There is also a way to change the default timeout time in the VS Code settings

[Kevin Buzzard]

I can't remember details but just go to settings and search for lean

[Michael Beeson]

I put it in the file. Had to knock a couple of zeroes off before it would "fit in a machine integer". Still got a timeout message.

[Michael Beeson]

Now I'll look for it in the settings.

[Michael Beeson]

If it's a legitimate timeout, it must be just barely timing out, because it gets to the last line and the last line should be trivial.
But I think there is something fishy about that.

[Mario Carneiro]

is it actually the last line?

[Mario Carneiro]

because if so it could be the result of kernel typechecking

[Mario Carneiro]

in particular if ifinish or some other tactic is producing a bad proof

[Michael Beeson]

The last line of the proof. Not the last line of the file.
And when I extracted two parts of the proof as lemmas, the timeout is at the last line of one of the lemmas.

[Mario Carneiro]

you won't notice that anything is wrong until all the metavariables are closed and the finished proof is pushed to the kernel for verification

[Michael Beeson]

Ah, so it could be that ifinish is not just taking too long, but is producing a bogus proof!

[Kevin Buzzard]

Here is a hypothesis. You are getting a timeout because you have inadvertently written some code that stinks, and if you're not going to post a minimal working example which exhibits the problem then nothing anyone says here is going to help you.

[Kevin Buzzard]

There are all sorts of tricks you can use to minimise your example, for example using axioms or constants instead of including previous proofs or definitions

[Michael Beeson]

OK, thanks for trying to help me.

[Kevin Buzzard]

One tiny typo can throw lean into a loop

[Michael Beeson]

Yes, but Lean isn't in a loop. If I don't type the last "exact" command, it processes the proof up to that point just fine. Then,
you can see that the goal and the last hypothesis are identical. So I don't see how I've written stinky code. But it does seem possible,
as Mario suggested, that my code "stinks" because 'ifinish' has produced a bogus proof. So, I think I'll try to eliminate the uses of
ifinish and see if I still have my problem. And if I do, then I'll try replacing all the referenced lemmas by axioms so I can create a MWE.
But I think that will take hours.

[Mario Carneiro]

"stinky code" doesn't mean logically incorrect

[Kevin Buzzard]

It could just mean one definition which doesn't quite do what you think it does

[Michael Beeson]

Well, I thought Kevin meant code that caused a timeout. But since I don't get a timeout right up until the last step...

[Mario Carneiro]

by the way, one way to minimize the proof is to replace subparts with sorry

[Mario Carneiro]

this will keep the proof compiling, and in particular going to the kernel, so you might be able to suss out a bad proof that way

[Michael Beeson]

Well, I may be slow here, but it seems to me that whatever I might have written, if I arrive at a point where the goal and one of my hypotheses are identical ( and there are no duplicate names of hypotheses) then it shouldn't matter what came before that.

[Michael Beeson]

Thanks Mario, I will try that as well as putting in axioms for lemmas.

[Mario Carneiro]

There are a number of reasons why that can cause a timeout, but it's hard to say for sure which reason is applicable unless you share some code with the bug

[Michael Beeson]

OK you guys have given me enough hints to follow up. Thank you very much. I'll let you know tomorrow what happened. It's bedtime now.

[Kevin Buzzard]

If your goal is X = X and you can't close it, try set_option pp.all true before your theorem. You might find that (a) they're not the same after all or (b) you have inadvertently made some gigantic terms

[Michael Beeson]

OK, so I went through and replaced all calls to ifinish with direct proofs. After that the timeout message is gone and everything is working fine. So, I guess Mario's theory that ifinish produced a bogus proof is the correct explanation. My code "stank" because ifinish stank.

[Patrick Massot]

I'm pretty sure you're the only user of this tactic, so not surprised at all that bug live there.

[Michael Beeson]

OK. But I humbly suggest that instead of "deterministic timeout" , a message like, "kernel failed to check proof" would have been helpful. Anyway, thanks to Mario and Kevin all is well.

[Johan Commelin]

@Michael Beeson but the kernel thought that if you gave it 5 more years, maybe it would have been able to check the proof after all...

[Michael Beeson]

Haha, that's wonderful!

[Johan Commelin]

Lean will tell you that the proof is wrong, if it is convinced that it's wrong. You hit an unlucky spot where Lean couldn't decide in a reasonable amount of time whether the proof was good or bad. Hence a timeout.

[Kevin Lacker]

i agree that "deterministic timeout" is an inaccurate name, mostly because it is not deterministic. it would be better to simply call it a "timeout"

[Kevin Buzzard]

I thought it was deterministic

[Kevin Lacker]

if you forget to run get-cache you can get timeouts on things that normally would be fine, for example. it is not a deterministic function of your code

[Mario Carneiro]

it is a deterministic function of the inputs to lean

[Mario Carneiro]

I think if you do a zero-edit on a failing proof in vscode it will not make it pass

[Mario Carneiro]

@Gabriel Ebner made a list of possible sources of nondeterminism before. I guess the unique names will be different, which could lead to a difference in some edge cases

[Kevin Lacker]

caching is the big one right? at least from what I can tell

[Mario Carneiro]

yes but that's easy to control and is a function of data on your HDD

[Mario Carneiro]

it's not a deterministic function of your code, but then again even the result of your code can depend on things like IO and unique names

[Ashvni Narayanan]

I am trying to prove the Noetherianess of a Dedekind domain (using the fractional ideals are invertible definition).

https://github.com/leanprover-community/mathlib/blob/de0bf7e02d1c4912e08982eeba8cb717a873da65/src/ring_theory/dedekind_domain.lean#L338

Whenever I try to put a sorry at the end of this proof, or anything that would solve the goal, I end up getting a deterministic timeout.

Any help is appreciated, thank you!

[Johan Commelin]

Can you split it into lemmas of <20 lines each?

[Johan Commelin]

That might make it more manageable

[Ashvni Narayanan]

Ok, I will try, thank you.

[Johan Commelin]

@Ashvni Narayanan Do you know about extract_goal?

[Johan Commelin]

It's a very useful tactic for things like this

[Ashvni Narayanan]

Yes, I see. I will try to use it, thank you.

[Ashvni Narayanan]

By the way, does it help to clear statements?

[Johan Commelin]

Probably not

[Kevin Lacker]

i would try replacing some of those simp statements in the middle of the proofs with simp only, it's easy to do and sometimes simp is slow

[Kevin Lacker]

i'm not sure how vscode displays it, but in emacs you can kind of see there are orange bars on the left while lean is compiling, and you can often figure out which parts of the proof are slow by watching those, and then you can optimize those parts

[Johan Commelin]

vscode has them too

[Ashvni Narayanan]

Yeah, I guess it might be the 4 line long suffices statement that might be causing the issue.

[Kevin Lacker]

"lemmas of 20 lines" might be more extreme than is absolutely necessary, i would be lazier about it and just break this up into 2 separate lemmas and see if that fixed it. and then if it still continued to not work, hopefully just 1 of the 2 is too slow, and then you can recurse

[Ashvni Narayanan]

I will try, thank you!

[Ashvni Narayanan]

Ok so I broke it up into two lemmas, it works perfectly fine till a certain goal, and then suddenly gives a deterministic timeout error only if I input a sorry or the statement that closes the goal. If I input something inaccurate, I see an error immediately. The lemma is about 25 lines long.

[Kevin Lacker]

can you paste just the lemma that's failing

[Kevin Lacker]

my guess is that some statement isn't compiling without the "sorry" because it needs some backward type inference or something weird like that before it'll start compiling

[Kevin Lacker]

what i would do here is, delete lines from the end of the slow proof and replace them with sorry, until i get something that works with sorry. then, probably the last bit you removed is the slow bit. when you say "it works perfectly fine until I write sorry", it isn't really working perfectly fine then, right? it's just not compiling at all because the code is ungrammatical.

[Kevin Lacker]

basically it would help to post both the "minimum not-working example" that doesn't compile, along with the "maximum working example", the point where your code does compile, you've just replaced a bunch of it with a sorry. the problem probably lies in the diff between those two states

[Ashvni Narayanan]

Thank you very much for your help. Turns out the lemma I was trying to use had the incorrect form. As soon as I fixed that, everything worked smoothly!