Lean become slow after the file reached 300~400 lines

Stream: new members

[Shanghe Chen]

Hi when reading MIL I found that if the file reached about 300~400 lines, it became quite slow. Any advise for avoding this? More specifically I got the problem from the following content linked here Is that becuase I used too many simp? If tagged more lemmas in this file with attribute simp, it even caused an error tactic 'simp' failed, nested error: (deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)

[Eric Wieser]

(note if you use gist.github.com rather than pastebin, you get lean syntax highlighting)

[Shanghe Chen]

Oh It's glad to know this. Update the link now :blush:

[Eric Wieser]

-- mark theses with attr simp really hurts the performance
-- and make timeout at 'whnf', maximum number of heartbeats (200000) has been reached:
@[to_additive
-- (attr := simp)
]
lemma Group₃.inv_inj {G : Type} [Group₃ G] {a b : G}(h: a⁻¹ = b⁻¹) : a = b := by

Yes, because you've sent simp on an infinite wild goose chase!

[Eric Wieser]

Whenever it sees a = b it now tries to prove a⁻¹ = b⁻¹, which it then tries to prove with a⁻¹⁻¹ = b⁻¹⁻¹, ...

[Eric Wieser]

Mathlib avoids this by stating the lemma as a⁻¹ = b⁻¹ ↔ a = b instead

[Shanghe Chen]

Oh I didn’t notice this, I found it problematic via uncommenting the attribute tag . It seems now only adding theorems to brackets of simp sometimes requires seconds for the goal changed in the Lean Infoview. Totally acceptable:blush:

[Vivek Rajesh Joshi]

I'm not sure if I should make my own topic or ask under this one, but this is exactly the problem that I'm facing. I have a function that calculates the row echelon form of a matrix, and it lies after 200 lines in my file. Running it for a 3x4 matrix is taking over a minute. However, if I copy the function over to a new file, where it lies after 150 lines, it takes only 8 seconds. I have a bunch of other functions and lemmas in the former file that aren't required for this function, but will be required later. How do I make this function faster while keeping all the contents of the file?

[Yaël Dillies]

Vivek Rajesh Joshi said:

it lies after 200 lines in my file. Running it for a 3x4 matrix is taking over a minute. However, if I copy the function over to a new file, where it lies after 150 lines, it takes only 8 minutes.

Are the numbers wrong maybe?

[Vivek Rajesh Joshi]

Whoops, sorry. I meant 8 seconds

[Shanghe Chen]

Yeah I found that sometimes I have to wait seconds if the proof is complicated or bad written. But I used a very old machine like

[Shanghe Chen]

OS: Arch Linux x86_64
Host: 20090 Lenovo IdeaPad Y470
Kernel: 6.8.9-arch1-2
Uptime: 13 hours, 8 mins
Packages: 828 (pacman)
Shell: zsh 5.9
Resolution: 1366x768
Terminal: /dev/pts/0
CPU: Intel i5-2430M (4) @ 3.000GHz
GPU: Intel 2nd Generation Core Processor Family
GPU: NVIDIA GeForce GT 550M
Memory: 5857MiB / 15940MiB

[Vivek Rajesh Joshi]

My laptop's pretty new and high-end. It's less than a year old, and is a HP Victus. Plus, I has no issue with running the function itself quickly, as shown with the latter file. The length of the former file is the problem.

[Shanghe Chen]

Vivek Rajesh Joshi said:

I'm not sure if I should make my own topic or ask under this one, but this is exactly the problem that I'm facing. I have a function that calculates the row echelon form of a matrix, and it lies after 200 lines in my file. Running it for a 3x4 matrix is taking over a minute. However, if I copy the function over to a new file, where it lies after 150 lines, it takes only 8 seconds. I have a bunch of other functions and lemmas in the former file that aren't required for this function, but will be required later. How do I make this function faster while keeping all the contents of the file?

May I ask what parameters are your hardware?

[Shanghe Chen]

OK got it

[Shanghe Chen]

There is a similar thread in PASE https://proofassistants.stackexchange.com/questions/1080/how-to-speed-up-lean the tips link is outdated though

[Shanghe Chen]

maybe check if the tips work https://web.archive.org/web/20240224061858/https://leanprover-community.github.io/tips_and_tricks.html

[Henrik Böving]

Vivek Rajesh Joshi said:

My laptop's pretty new and high-end. It's less than a year old, and is a HP Victus. Plus, I has no issue with running the function itself quickly, as shown with the latter file. The length of the former file is the problem.

You will have to show your work if you expect people to figure this type of performance stuff out.

[Shanghe Chen]

Yeah posting codes or #MWE may help

[Vivek Rajesh Joshi]

The file's pretty long and has an import to another file, so I'll post the link to the file in my GitHub repo: https://github.com/vivek-rj/gauss_elim1/blob/master/GaussElim/ge_test2vec.lean

[Kevin Buzzard]

If you cannot make a reproduction without having other people download your project, could you perhaps upload a file into your project which indicates the problem? Right now you're saying "please clone my repo and solve my problem which is somewhere in this file", which is a bad way to ask a question. Perhaps two files which indicate something working and something not working?

[Vivek Rajesh Joshi]

Yes, sorry. I only uploaded the long file. Here's the short file, where the function application runs in 8 seconds: https://github.com/vivek-rj/gauss_elim1/blob/master/GaussElim/mwetest.lean
The function application is written as this line:
#eval rowEchelonList_ij' (m:=3) (n:=4) (by linarith) (by linarith) amat 0 0

[Kevin Buzzard]

So you have two files in your repo, one of which is 150 lines long and the other is 230 lines long, and you're running what looks like the same command twice (although you're #evaling a declaration which is defined in both files). What's the difference between the two files? I suspect this has nothing to do with whether you have 230 lines or 150 lines --- that's I suspect a red herring. There is something in the bad file which is making things bad.

[Kevin Buzzard]

You could probably debug this yourself by removing things in the bad file until it's quick, and then report on which declaration is making it slow.

[Vivek Rajesh Joshi]

I see. I thought that since the other lines don't contribute to the function in the long file, they just act as extra lines in the code from the point of view of the function. I'll try removing them and see which of them has an impact.

[Kevin Buzzard]

They clearly do contribute to it somehow, because they're making it take 6 times longer to run!

[Eric Wieser]

When you say "it takes longer to run", do you mean "when I run it on the command line, it takes longer to run the whole file", or "the time between starting the #eval and finishing it takes longer"? you can use set_option trace.profiler true in to measure the time of a single command, which might be more precise than what you're doing

[Kevin Buzzard]

I cloned the project and it seemed to me like there were two #evals which ostensibly looked like they were doing the same thing but one was taking much longer than the other.