Performance much worse in Windows than in WSL

[PratherConid]

Description

Executing the same Lean code ~200 times slower on Windows than on WSL.

Steps to Reproduce

Do Step 1, 2 & 3 in WSL and Windows. Step 1 & 2 show the raw issue, and Step 3 shows a somewhat minimized example.

1. git clone https://github.com/avigad/lean-auto.git
2. Open Test/Test_regression.lean, check the time took by the example

  -- In `Checker Statistics`, check that the `assertions` field is `1`
  set_option auto.optimizeCheckerProof true in
  set_option trace.auto.buildChecker true in
  example (h₁ : False) (h₂ : a = b) : False := by auto [h₁, h₂]

3. Create a new file in Test/ with the following content:

import Auto

open Lean in
def test : MetaM Unit := do
  let startTime ← IO.monoMsNow
  let expr := Expr.app (.const ``Not []) (.const ``True [])
  let _ ← Meta.withDefault <| Meta.whnf expr
  IO.println s!"{(← IO.monoMsNow) - startTime}"

#eval test

Check the output of #eval test. Then, replace the first line import Auto with import Lean, and check the output of #eval test again.

Versions

leanprover/lean4:v4.3.0-rc1
WSL: Ubuntu 20.04.6 LTS
Windows: Windows 11

[kim-em]

Do you think you could minimize this so that all we need to do to observe the effect is run

git clone X
time lake build

on different OSs?

[PratherConid]

@semorrison I don't know how to minimize it to bare shell command.
After further investigation, I found that the issue only occurs when I open the file in VSCode (probably indicates that the issue is related to lean server). Anyway, I've created a repo https://github.com/PratherConid/lean-perf. We can clone, build, and observe the time of lake env lean Perf/Test_Regression.lean using the following command:

Linux (I've only tested this on WSL):

git clone https://github.com/PratherConid/lean-perf.git; cd lean-perf; lake build; time lake env lean Perf/Test_Regression.lean

Windows:

git clone https://github.com/PratherConid/lean-perf.git; cd lean-perf; lake build; Measure-Command {start-process (lake env lean Perf/Test_Regression.lean) -wait}

Note that lake build might fail because of linker failure, but that does not affect the latter lake env ....
On my computer the running time of lake env ... does not show significant difference. However, if I open Perf/Test_Regression.lean in VSCode, there is significant performance difference between Linux and Windows.
p.s. Please let me know if there is a way to invoke lean server (or anything lean uses in VSCode) through shell command.

[kim-em]

% time lake env lean Perf/Test_Regression.lean
lake env lean Perf/Test_Regression.lean  16.28s user 1.59s system 96% cpu 18.538 total

However lake build on Windows fails with

ld.lld: error: too many exported symbols (got 76583, max 65535)

(This is #2346.)

I'm surprised you could even get it to build at all on Windows!

[PratherConid]

My comment previously:

Note that lake build might fail because of linker failure, but that does not affect the latter lake env ....

[PratherConid]

(I think linker failure is irrelevant

[kim-em]

On windows I get (after the linker failure)

> Measure-Command {start-process (lake env lean Perf/Test_Regression.lean) -wait}
Inhabitation
MonomorphizationWierdExample
DSRobust
CollectLemma
Skolemization
Extensionalization
UnfoldConst
Basic
HigherOrder
Polymorphic
MetaVaraible
TypeDefeq
DefinitionRecognition
Adhoc
Start-Process : Cannot convert 'System.Object[]' to the type 'System.String' required by parameter 'FilePath'.
Specified method is not supported.
At line:1 char:32
+ ... mmand {start-process (lake env lean Perf/Test_Regression.lean) -wait}
+                          ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    + CategoryInfo          : InvalidArgument: (:) [Start-Process], ParameterBindingException
    + FullyQualifiedErrorId : CannotConvertArgument,Microsoft.PowerShell.Commands.StartProcessCommand



Days              : 0
Hours             : 0
Minutes           : 0
Seconds           : 43
Milliseconds      : 954
Ticks             : 439543499
TotalDays         : 0.00050873090162037
TotalHours        : 0.0122095416388889
TotalMinutes      : 0.732572498333333
TotalSeconds      : 43.9543499
TotalMilliseconds : 43954.3499

[PratherConid]

Yes. The output you get from linux/windows looks similar to the one I got.

[PratherConid]

@semorrison I saw you marked this issue as "invalid". Does that mean the issue description is not good enough? Or you cannot reproduce the issue? Note that the current issue is not the performance difference between the lake build or the lake env command on different OSs. The issue is that if we open Perf/Test_Regression.lean using VSCode on different OSs, there is significant performance difference elaborating the entire file.
Sorry for the confusing error message. We can replace Measure-Command {start-process (lake env lean Perf/Test_Regression.lean) -wait} with Measure-Command {lake env lean Perf/Test_Regression.lean}. The latter does not produce the above error message. (But again, the lake env ... command does not manifest the current issue) I could try to get rid of the linker error by minimizing the example, but that would be difficult.

[kim-em]

Yes, I'm unconvinced there is a reproducible problem here that anyone could work with, particularly given the linker errors.

[Kha]

Isn't the linker error just from [default_target]ing the lean_exe, which is not relevant for the issue? If you move it to the lean_lib, I would hope the issue persists but without any build errors

[Kha]

For what it's worth, I have no idea why on Windows the server could be slower here than the cmdline...

[PratherConid]

I've moved [default_target]. Now the build error is gone, and the issue persists on my computer. After

git clone https://github.com/PratherConid/lean-perf.git; cd lean-perf; lake build

the stats are as follows:

Linux

• time lake env lean Perf/Test_Regression.lean

Auto found proof. Time spent by auto : 137ms
...(omitted)
real    0m33.241s
user    0m21.840s
sys     0m0.933s

• Server (open Perf/Test_Regression.lean in VSCode, wait for it to elaborate the entire file): 16 Seconds (stopwatch)

Windows

• Measure-Command { lake env lean .\Perf\Test_Regression.lean }

Inhabitation
MonomorphizationWierdExample
...(omitted)
TotalSeconds      : 62.8786204
TotalMilliseconds : 62878.6204

• Server (open Perf/Test_Regression.lean in VSCode, wait for it to elaborate the entire file): 287 Seconds (Stopwatch)

Versions

leanprover/lean4:v4.3.0-rc1
Linux: Ubuntu 20.04.6 LTS (WSL)
Windows: Windows 11 Home

[Kha]

I'm removing the invalid label based on the information above

[Kha]

I get

WSL 33s
Windows 38s
Windows language server 51s

so I think we can consider this issue nonreproducible; try checking your virus scanner etc?

The language server overhead could be independently investigated but likely is not limited to Windows.