feat(CI): add -T100000 to the build step in CI (#2276)
This PR adds `-T100000` to CI. This is the default timeout setting in the VS Code extension and emacs.
With some exceptions, noted with `FIXME` comments mentioning `-T50000`, the library now compiles with `-T50000`:
- [ ] `has_sum.has_sum_ne_zero` in `src/topology/algebra/infinite_sum.lean`, where I don't really understand why it is slow.
- [ ] `exists_norm_eq_infi_of_complete_convex` in `src/analysis/normed_space/real_inner_product.lean`, which has a giant proof which should be rewritten in several steps.
- [ ] `tangent_bundle_core.coord_change_comp` in `src/geometry/manifold/basic_smooth_bundle.lean`.
- [ ] `change_origin_radius` in `src/analysis/analytic/basic.lean`
There are 3 `def`s related to category theory which also don't compile:
- [ ] `adj₁` in `src/topology/category/Top/adjunctions.lean`
- [x] `cones_equiv_inverse` in `src/category_theory/limits/over.lean` (addressed in #2840)
- [ ] `prod_functor` in `src/category_theory/limits/shapes/binary_products.lean`
This proof no longer causes problems with `-T50000`, but it should still be broken up at some point.
- [ ] `simple_func_sequence_tendsto` in `src/measure_theory/simple_func_dense.lean`, which has a giant proof which should be rewritten in several steps. ~~This one is really bad, and doesn't even compile with `-T100000`.~~
[Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/-T50000.20challenge).
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
