[Merged by Bors] - refactor(linear_algebra): morphism refactor for linear_equiv, continuous_linear_equiv, linear_isometry and linear_isometry_equiv
#15078
Conversation
dupuisf
added
the
awaiting-review
|
The morphism refactor part looks good, but I'd like to see a bit more work being done to address the timeout. @sgouezel, since you appear in the blame of both proofs that are timing out, do you have any suggestions? |
|
I did some additional digging into the timeout problem in I don't have time to debug this myself before going on vacation, so I just thought I would record this here for now. |
|
This has been discussed in Zulip, in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/has_coe_to_fun.20instance.20search/near/291439013. The issue is that Lean tries to find a coercion to function spaces when the target is a pi type, including |
|
bors r+ |
github-actions
bot
added
ready-to-merge
…inuous_linear_equiv`, `linear_isometry` and `linear_isometry_equiv` (#15078) This PR brings the morphism refactor to `linear_equiv`, `continuous_linear_equiv`, `linear_isometry`, and `linear_isometry_equiv`. Note that I had to resort to an ugly hack to deal with deterministic timouts in two proofs: `vitali.exists_disjoint_covering_ae` and another one in the counterexamples folder. Both of these are very large proofs with no obvious sublemmas to extract or inefficiencies, so I just used `try_for 20000 {...}` to increase the timeout. It's not great, but I don't see a better alternative -- besides, I don't think it's unreasonable for long proofs like these to have a bigger timeout. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
|
Build failed (retrying...): |
…inuous_linear_equiv`, `linear_isometry` and `linear_isometry_equiv` (#15078) This PR brings the morphism refactor to `linear_equiv`, `continuous_linear_equiv`, `linear_isometry`, and `linear_isometry_equiv`. Note that I had to resort to an ugly hack to deal with deterministic timouts in two proofs: `vitali.exists_disjoint_covering_ae` and another one in the counterexamples folder. Both of these are very large proofs with no obvious sublemmas to extract or inefficiencies, so I just used `try_for 20000 {...}` to increase the timeout. It's not great, but I don't see a better alternative -- besides, I don't think it's unreasonable for long proofs like these to have a bigger timeout. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
linear_equiv, continuous_linear_equiv, linear_isometry and linear_isometry_equivlinear_equiv, continuous_linear_equiv, linear_isometry and linear_isometry_equiv
This PR brings the morphism refactor to
linear_equiv,continuous_linear_equiv,linear_isometry, andlinear_isometry_equiv.Note that I had to resort to an ugly hack to deal with deterministic timouts in two proofs:
vitali.exists_disjoint_covering_aeand another one in the counterexamples folder. Both of these are very large proofs with no obvious sublemmas to extract or inefficiencies, so I just usedtry_for 20000 {...}to increase the timeout. It's not great, but I don't see a better alternative -- besides, I don't think it's unreasonable for long proofs like these to have a bigger timeout.