-
Notifications
You must be signed in to change notification settings - Fork 298
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(CI): add -T100000 to the build step in CI #2276
Conversation
Fixed. Actually, I should move those changes to a separate PR, in any case. |
Now blocked on #2393, which contains the fixes to two theorems that I'd previously pushed here. |
Refactor two proofs to bring them under `-T50000`, in the hope that we can later add this requirement to CI, per #2276.
Now it fails in |
Yes, |
Refactor two proofs to bring them under `-T50000`, in the hope that we can later add this requirement to CI, per leanprover-community#2276.
Refactor two proofs to bring them under `-T50000`, in the hope that we can later add this requirement to CI, per leanprover-community#2276.
Wow, mathlib builds with 100000 again, I guess because of the changes in Lean 3.13. I've changed it to 50000 again (and disabled finding the olean cache to make the build more honest) to see what happens. |
I think that we should add |
Agreed. I'll see if I can mark the new T50000 failures with FIXME. |
bors r+ |
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>
Pull request successfully merged into master. Build succeeded: |
cf. #2276. This will also prevent some confusing timeouts, see e.g. https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Tests.20fail
Refactor two proofs to bring them under `-T50000`, in the hope that we can later add this requirement to CI, per leanprover-community#2276.
…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 leanprover-community#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>
cf. leanprover-community#2276. This will also prevent some confusing timeouts, see e.g. https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Tests.20fail
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
insrc/topology/algebra/infinite_sum.lean
, where I don't really understand why it is slow.exists_norm_eq_infi_of_complete_convex
insrc/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
insrc/geometry/manifold/basic_smooth_bundle.lean
.change_origin_radius
insrc/analysis/analytic/basic.lean
There are 3
def
s related to category theory which also don't compile:adj₁
insrc/topology/category/Top/adjunctions.lean
cones_equiv_inverse
insrc/category_theory/limits/over.lean
(addressed in [Merged by Bors] - chore(category_theory): T50000 challenge #2840)prod_functor
insrc/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
insrc/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.