lean failing on large proofs

Stream: general

[Jeremy Avigad]

I am working on a code verification project with a number of large proofs. I recently updated Lean andmathlib from much older versions, and now I am experiencing the following behavior. The development gets stuck on a large file when I run lean --make, which is to say, the output freezes, the system monitor shows a cpu maxing out, and the fan keeps whirring. But when I open the file in VS Code, the yellow bars disappear after about a minute and everything looks o.k. I can step through the file and see the goals change in the infoview.

Does anyone have any thoughts as to how I can debug, and what might explain the success of the lean server in contrast to lean from the command line? If I type lean --help, I see all kinds of options to increase various limits, but I have no idea what are reasonable numbers to type.

[Mario Carneiro]

you could turn on the profiler in the file using set_option profiler true which should at least narrow the issue down to a specific proof, and may also pinpoint a bad tactic if that's the culprit

[Jeremy Avigad]

Thanks for the suggestion. The file has a single theorem, a computer-generated proof of close to 500 lines, that uses simp and norm_num a lot to step through computations. Before lean --make freezes, the profiler reports that the elaborator succeeded in 78.3 seconds, so it seems that it is the kernel check that fails. (There is no smoking gun in the report from the profiler; it shows a lot of time spent in simp and norm_num, as expected.)

The proof has a couple of calculations with 80-digit numbers, so there is plenty of room for the kernel to get lost. In the mathlib upgrade, I had to fix some problems that had to do with casts from nat to int to a field, so the problem may have to do with that. I will experiment.

Is there anything to explain why the kernel check seems to work in VS Code but not from the command line?

[Ruben Van de Velde]

Just guessing: does vscode pass any interesting command line options to lean that you don't use from the command line?

[Julian Berman]

It raises -M and -T (memory and timeout) if you happen not to be passing those -- the defaults at the minute are -M 4096 and -T 100000 (from https://github.com/leanprover/vscode-lean/blob/8ca7fa689bc89f5d327a4d00017855e3ede0561b/package.json#L32-L50)

[Johan Commelin]

Does it help to start squeezing simps?

[Johan Commelin]

Do we need a squeeze_norm_num?

[Jeremy Avigad]

Thanks, Julian, I'll try messing around with the limits. Johan, virtually all our simps are squeezed, and generally we even use norm_num1 instead of norm_num.

[Johan Commelin]

Hmmzz... then it must be a truly gigantic proof (-;

[Jeremy Avigad]

The problem is solved. Here's the resolution.

First, the problem was not in the file I thought it was, but in a dependency. There was a proof that passed the elaborator but led to a deterministic timeout in the kernel. VS Code compiled the later file without noticing the timeout (I guess the type signature was enough) and lean --make worked on parts in parallel, so it froze on the earlier dependency just after announcing the successful completion of the later one. Go figure.

Second, the real problem was simply a numeric calculation with large nat numeral cast to int. If you are not careful (e.g. if you use the simplifier or force definitional reduction) Lean falls into unary notation. Using the right simp only rules avoids that. I have gotten used to dealing with that, but this bit of code was written by a colleague who was not aware of the issue.

Everything works great now. :smile: Thanks everyone for the help.

[Jeremy Avigad]

To illustrate, the first proof below takes a number of seconds, whereas the second is instantaneous:

example: ((12345678901234567890123456789012345678901234567890 : ℕ) : ℤ) + 1 =
  12345678901234567890123456789012345678901234567891 :=
by norm_num

example: ((12345678901234567890123456789012345678901234567890 : ℕ) : ℤ) + 1 =
  12345678901234567890123456789012345678901234567891  :=
begin
  simp only [int.coe_nat_zero, int.coe_nat_one, int.coe_nat_bit0, int.coe_nat_bit1],
  norm_num1
end

[Alex J. Best]

Julian Berman said:

It raises -M and -T (memory and timeout) if you happen not to be passing those -- the defaults at the minute are -M 4096 and -T 100000 (from https://github.com/leanprover/vscode-lean/blob/8ca7fa689bc89f5d327a4d00017855e3ede0561b/package.json#L32-L50)

I think the default for lean --make is timeout and memory = 0 (aka infinite) though without extra options, so vscode settings are only there to tame lean

[Sebastien Gouezel]

Jeremy Avigad said:

To illustrate, the first proof below takes a number of seconds, whereas the second is instantaneous:

Is that something that could be fixed in norm_num?

[Jeremy Avigad]

The plot thickens. The proof by simp; norm_num has the same slow behavior, but if I squeeze that simp, Lean tells me to use simp only [int.coe_nat_bit0, int.coe_nat_bit1, nat.cast_one], norm_num, which has the fast behavior. So I guess simp is backtracking? Let me check...

[Jeremy Avigad]

The trace is huge. Trying a smaller example 100 + 1 = 101 shows that the simplifier is trying all kinds of crazy things because the head symbol coe matches a lot. That explains why elaboration would be slow, but it doesn't explain our deterministic timeout.

I extracted the three big calculations below from the proof that was giving me a deterministic timeout. Replacing the proofs by sorry allowed the proof to compile. But separated out, none of them are problematic, and what squeeze simp tells me to do to speed it up is essentially what I did to fix the proof. So I really don't know why those calculations seemed to result in a failure in the kernel check rather than in the elaboration phase.

So maybe I was wrong, the problem wasn't with the kernel check, just too much time elaborating calculations in an already long proof?

Anyhow, it seems that the only way to solve the problem with norm_num is to avoid the use of the full-blown version of simp for preprocessing.

example : (19342813113834066795298816 * (4 : ℤ) - ↑(2 ^ 86 : ℕ)) % ↑(3618502788666131213697322783095070105623107215331596699973092056135872020481 : ℕ) = 0 :=
by norm_num

example : (19342813113834066795298816 * (4 : ℤ) - ↑(2 ^ 86 : ℕ)) % ↑(3618502788666131213697322783095070105623107215331596699973092056135872020481 : ℕ) = 0 :=
by norm_num

example : ((2^86 : ℕ) : ℤ) * -46768052394588894761721767695234645457402928824320 % ↑(3618502788666131213697322783095070105623107215331596699973092056135872020481 : ℕ) = 1 :=
by norm_num

Incidentally, in case you are curious, I have discovered that you can Google 3618502788666131213697322783095070105623107215331596699973092056135872020481.

[Jeremy Avigad]

One last plot twist. I turns out that I oversimplified my examples. The large prime was hidden behind a definition, and my colleague used dsimp to unfold it, as in the example below. It produces a deterministic timeout in the kernel checking phase. Replacing dsimp by rw is slow but succeeds.

def PRIME := 3618502788666131213697322783095070105623107215331596699973092056135872020481

example : (2^86 : ℤ) * -46768052394588894761721767695234645457402928824320 % ↑PRIME = 1 :=
by dsimp [PRIME]; norm_num

[Junyan Xu]

You could also hack your car by googling MIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEAy8Dbv8prpJ : https://programmingwithstyle.com/posts/howihackedmycar/

[Mario Carneiro]

FYI, norm_num has no support for coe, so this is mostly simp behavior being observed