chore: add LNSym omega benchmarks with large problems that take multiple seconds to solve

[bollu]

trafficstars

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5dea30f169b91cdda9a3903a7a9d125e0f075605 --onto a4fda010f3d44c02393d5afd5cf05509989daf63. (2024-10-04 20:01:17)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5dea30f169b91cdda9a3903a7a9d125e0f075605 --onto 9dac514c2fc80d3f60076314ad30a993a7b2c22f. (2024-10-07 22:23:28)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 248864c716e4276da7135de2b624a7b6b198f50c --onto 3e75d8f74297bc258352f8d89f71496aacefe7ae. (2024-10-08 20:12:54)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 248864c716e4276da7135de2b624a7b6b198f50c --onto b814be6d6a5334784b172db15fd7fea39b4e3233. (2024-10-10 04:35:50)

[hargoniX]

!bench

[hargoniX]

Oh this is not going to work yet, you need to add it to the bench configuration of course, my bad.

[leanprover-bot]

Here are the benchmark results for commit 4bf37d0a653bdf234bead6e74cba1bc09a139ee5. There were significant changes against commit 5dea30f169b91cdda9a3903a7a9d125e0f075605:

  Benchmark       Metric          Change
  ===============================================
- bv_decide_mul   branch-misses     2.9% (16.5 σ)

[hargoniX]

!bench

[leanprover-bot]

Here are the benchmark results for commit d4808ba9d67c026d0020e4ba59deabf343a810e8. The entire run failed. Found no significant differences.

[hargoniX]

Typo in your file name.

[hargoniX]

!bench

[leanprover-bot]

Here are the benchmark results for commit 5eaf27fa2cbf263fcba0b63ff59d727ddb47223a. There were significant changes against commit 248864c716e4276da7135de2b624a7b6b198f50c:

  Benchmark       Metric       Change
  ============================================
- bv_decide_mul   task-clock     1.2% (10.7 σ)
- bv_decide_mul   wall-clock     1.7% (20.9 σ)

[bollu]

omega10 claims to take 3.3s in instantiate metavars from inside VScode/nvim, but externally when run with lean, takes 195ms. Is this a time leak?

I tried to measure this with an actual watch, but I would like a more reliable method that an literal wall clock to measure difference between time-in-IDE versus time-in-batch (this is easy, use time).

[hargoniX]

!bench

[leanprover-bot]

Here are the benchmark results for commit f14c278cee90ee289b84eb706e9bf237f41a4dd7. There were no significant changes against commit 248864c716e4276da7135de2b624a7b6b198f50c.

[shigoel]

For sanity checking, I reproduced @bollu's benchmarks for omega10.lean. The numbers agree.

In batch mode:

lean omega10.lean
omega10.lean:12:1: warning: unused variable `h_upper_bound`
note: this linter can be disabled with `set_option linter.unusedVariables false`
tactic execution of Lean.Parser.Tactic.omega took 944ms
instantiate metavars took 214ms
share common exprs took 210ms
type checking took 373ms
elaboration took 103ms
cumulative profiling times:
	attribute application 0.00108ms
	elaboration 103ms
	fix level params 8.81ms
	instantiate metavars 214ms
	linting 26.1ms
	parsing 1.03ms
	process pre-definitions 64.9ms
	share common exprs 210ms
	simp 20.6ms
	tactic execution 946ms
	type checking 373ms
	typeclass inference 62.2ms

In VSCode:

tactic execution of Lean.Parser.Tactic.omega took 951ms
instantiate metavars took 2.63s
share common exprs took 1.03s
type checking took 472ms
linting took 124ms
elaboration took 631ms

[bollu]

I'm not sure how to get these files tracked on http://speed.lean-fro.org/lean4/run-detail/b07e1b73-1c45-4917-9065-41b479f55c6c. I guess that someone will need to teach it to also track speedcenter tests labeled omega?

[bollu]

I added an example that shows a fairly dramatic difference in time between the shell and VSCode:

Shell: 1.59s versus VSCode: 18.5s for "instantiate metavars".

---

tactic execution of Lean.Parser.Tactic.omega took 4.3s instantiate metavars took 1.97s share common exprs took 1.59s type checking took 1.35s process pre-definitions took 1.85s linting took 127ms elaboration took 690ms cumulative profiling times: attribute application 0.00283ms elaboration 690ms fix level params 46.1ms instantiate metavars 1.97s linting 127ms parsing 2.07ms process pre-definitions 1.85s share common exprs 1.59s simp 18.7ms tactic execution 4.3s type checking 1.35s typeclass inference 299ms

tactic execution of Lean.Parser.Tactic.omega took 4.08s instantiate metavars took 18.5s share common exprs took 5.04s type checking took 1.09s process pre-definitions took 1.14s linting took 382ms elaboration took 3.06s