CI hangs at "test mathlib"

Stream: mathlib4

[Michael Stoll]

In #29218, it looks like CI hangs at the "test mathlib" stage. The output I see (here) is

Run cd pr-branch
+ cd pr-branch
+ lake --iofail test
✔ [1398/1658] Built MathlibTest.Replace (365ms)
✔ [2760/2999] Built MathlibTest.InferParam (431ms)
✔ [2982/2999] Built MathlibTest.UnusedTactic (530ms)
✔ [2984/3000] Built MathlibTest.Have (544ms)
✔ [2985/3000] Built MathlibTest.DocString (598ms)
✔ [2987/3312] Built MathlibTest.choose_reduction (1.1s)
✔ [2988/3312] Built MathlibTest.BigOps (1.1s)
✔ [3302/3731] Built MathlibTest.success_if_fail_with_msg (731ms)
✔ [4307/4701] Built MathlibTest.itauto (1.1s)
✔ [4693/5118] Built MathlibTest.ModuleCasing (611ms)
✔ [6405/6678] Built MathlibTest.Complex (2.1s)
✔ [7162/7267] Built MathlibTest.finiteness (2.6s)
✔ [7163/7267] Built MathlibTest.fun_prop_dev (2.7s)
✔ [7164/7267] Built MathlibTest.Use (1.1s)
✔ [7165/7267] Built MathlibTest.polyrith (1.1s)
✔ [7166/7267] Built MathlibTest.CategoryTheory.MonoidalComp (1.1s)
✔ [7167/7267] Built MathlibTest.CategoryTheory.ToApp (1.3s)
(...)
✔ [7424/7462] Built MathlibTest.deriving_countable (1.3s)
✔ [7425/7462] Built MathlibTest.enat_to_nat (1.2s)
✔ [7426/7462] Built MathlibTest.linarith (12s)
✔ [7427/7462] Built MathlibTest.norm_num_rpow (1.5s)
✔ [7428/7462] Built MathlibTest.conv (467ms)
✔ [7429/7462] Built MathlibTest.mod_cases (1.0s)
✔ [7430/7462] Built MathlibTest.Contrapose (786ms)
✔ [7431/7462] Built MathlibTest.DefEqTransformations (888ms)
✔ [7432/7462] Built MathlibTest.eval_elab (1.2s)
✔ [7433/7462] Built MathlibTest.DeprecateTo (514ms)
✔ [7434/7462] Built MathlibTest.rsuffices (789ms)
✔ [7435/7462] Built MathlibTest.Monotonicity (1.5s)
✔ [7436/7462] Built MathlibTest.apply_congr (922ms)
✔ [7437/7462] Built MathlibTest.ErwQuestion (469ms)
✔ [7438/7462] Built MathlibTest.Find (10s)
✔ [7439/7462] Built MathlibTest.linear_combination (6.4s)
✔ [7440/7462] Built MathlibTest.linear_combination' (3.6s)
✔ [7441/7462] Built MathlibTest.antidiagonal (2.1s)
✔ [7442/7462] Built MathlibTest.Clear_ (388ms)
✔ [7443/7462] Built MathlibTest.ClearExclamation (488ms)
✔ [7444/7462] Built MathlibTest.SplitIfs (614ms)
✔ [7445/7462] Built MathlibTest.apply_fun (1.5s)
✔ [7446/7462] Built MathlibTest.recover (371ms)
✔ [7447/7462] Built ProofWidgets (533ms)
✔ [7448/7462] Built MathlibTest.nontriviality (1.2s)
✔ [7449/7462] Built MathlibTest.ApplyAt (1.2s)
✔ [7450/7462] Built MathlibTest.apply_rules (1.1s)
✔ [7451/7462] Built MathlibTest.abel (2.4s)
✔ [7452/7462] Built MathlibTest.DeprecatedModuleTest (396ms)
✔ [7453/7462] Built MathlibTest.CommDiag (935ms)
✔ [7454/7462] Built MathlibTest.StringDiagram (1.3s)
✔ [7455/7462] Built MathlibTest.tactic_timeout (7.6s)
✔ [7456/7462] Built MathlibTest.norm_num (7.6s)
✔ [7457/7462] Built MathlibTest.TautoSet (6.0s)
✔ [7458/7462] Built MathlibTest.import_all (2.9s)
✔ [7459/7462] Built MathlibTest.MathlibTestExecutable (2.0s)
✔ [7460/7462] Built MathlibTest.reduce_mod_char (16s)

and then nothing further seems to happen (this step has been running for 15 minutes now; I had canceled and restarted the workflow previously in the hope that it was a transient issue).

Any idea what could cause this?

[Michael Stoll]

It did actually finish after a bit more than half an hour. The last line is

✔ [7461/7462] Built MathlibTest.sqrt (1973s)

Can this be related to the new docs#Nat.ratSqrt ? @Kim Morrison

[Robin Arnez]

Well the test works with a 1 million digit number...

[Kim Morrison]

Hmmmm, it runs very quickly locally for me. I'll take a look.

[Kim Morrison]

I've double checked that it runs within seconds on my machine, but indeed CI takes 30 minutes. I will remove the test while investigating.

[Kim Morrison]

I remain mystified here. I've checked that the test is fast on my machine (macos), on chonk (linux), on hoskinson (the CI runner, linux), and even on hoskinson under the landrun wrapper.

[Yakov Pechersky]

Could it be a memory issue during the ci run, such that it has to hit swap a lot?

[Kim Morrison]

Woah... on any of the above machines:

• lake env lean MathlibTest/sqrt.lean is fast
• lake build MathlibTest is fast
• lake test is super slow

[Kim Morrison]

chore: temporarily turn off mysteriously slow test #29226

until we work it out...