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

[bollu]

No description provided.

[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 4bf37d0.
There were significant changes against commit 5dea30f:

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

[hargoniX]

!bench

[leanprover-bot]

Here are the benchmark results for commit d4808ba.
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 5eaf27f.
There were significant changes against commit 248864c:

  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 f14c278.
There were no significant changes against commit 248864c.

[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