Extreme runtime increase

[gebner]

The latest timeouts don't seem to be caused by a simple infinite loop. It's just that many files now take a lot longer than they used to. For example here is what's running right now:

nawrocki 3359171  100  2.2 880888 745396 ?       R    18:19  74:21 /home/lean/actions-runner/_work/mathport/mathport/build/bin/mathport config.json Mathbin::data.analysis.filter
nawrocki 3359253  100  2.4 953668 805644 ?       R    18:24  69:35 /home/lean/actions-runner/_work/mathport/mathport/build/bin/mathport config.json Mathbin::category_theory.sites.pretopology
nawrocki 3359429  100  2.2 890620 747472 ?       R    18:38  55:47 /home/lean/actions-runner/_work/mathport/mathport/build/bin/mathport config.json Mathbin::data.set.semiring
nawrocki 3360243  100  2.4 937048 796800 ?       R    19:10  23:43 /home/lean/actions-runner/_work/mathport/mathport/build/bin/mathport config.json Mathbin::group_theory.subgroup.basic
nawrocki 3360548  100  2.2 893600 755460 ?       R    19:29   4:35 /home/lean/actions-runner/_work/mathport/mathport/build/bin/mathport config.json Mathbin::order.pfilter
nawrocki 3360575  100  2.4 939660 794580 ?       R    19:31   3:03 /home/lean/actions-runner/_work/mathport/mathport/build/bin/mathport config.json Mathbin::topology.sets.closeds
nawrocki 3360604  100  2.7 1063676 913580 ?      R    19:31   2:58 /home/lean/actions-runner/_work/mathport/mathport/build/bin/mathport config.json Mathbin::topology.sheaves.presheaf
nawrocki 3360636  100  2.4 950564 799544 ?       R    19:32   1:39 /home/lean/actions-runner/_work/mathport/mathport/build/bin/mathport config.json Mathbin::geometry.manifold.charted_space

data.analysis.filter has been running for 75 minutes and is not finished yet, but I think it will finish at some point. To compare, topology.local_homeomorph was running for 20 minutes but finished then.

This seems to be due to a mathlib change between August 23 (successful build) and August 25 (first timeout). As far as I can tell, nothing changed on the mathport end.

[gebner]

category_theory.sites.pretopology finished after more than an hour of runtime.

[digama0]

Can we add timing info to the mathport logs? For example, the time taken for binport and synport on each file. Also, it doesn't seem like the mathlib commit is available from the logs - I can only find the commits for lean3, lean4, and mathlib4.

[gebner]

I've added the mathlib commit info to both the log as well as the predata tarball.

I'm not sure if the timing is helpful. But at least we can now try this out locally:

./download-predata.sh predata-nightly-2022-08-26
rm -rf Outputs
./build/bin/mathport --make config.json Mathbin::data.analysis.filter

[gebner]

Hooked up a profiler to order.filer.basic:

# Children      Self  Command   Shared Object      Symbol
    99.93%     2.40%  mathport  mathport           [.] lean::csimp_fn::is_recursive_fn::visit

I guess we accidentally (?) made some function computable in mathlib and now we're running the compiler on everything.

[digama0]

I think we should probably force_noncomputable everything in mathbin. The terms are not appropriate for evaluation by lean 4 and it's a bit dangerous to assume they are. (If that's too heavy a hammer, we could put a small timeout on the compiler and give up otherwise.)

[gebner]

Hmm, now it hangs at ζ-reduction in number_theory.bertrand (bertrand.real_main_inequality to be specific).

   100.00%     0.00%  mathport  mathport           [.] l_Lean_Meta_transform_visit___at_Lean_Meta_zetaReduce___spec__2___lambda__1

[Kha]

Oh, is this with https://github.com/leanprover/lean4/pull/1512? That would at least explain zetaReduce potentially taking longer (because it should be more correct now).

[gebner]

No, without. Maybe 1512 fixes this issue.