chore(topology/sheaves/sheaf_condition): first pass at speeding up #4832
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
There are still a bunch of things that take 10-15s on my machine. But I don't see easy ways to speed them up. (In total, these three files took up multiple minutes to compile, and it's still not great.)
jcommelin
added
the
awaiting-review
kbuzzard
reviewed
Oct 31, 2020
| @@ -137,6 +137,7 @@ instance (V : opens_le_cover U) : | |||
| nonempty (comma (functor.from_punit V) (pairwise_to_opens_le_cover U)) := | |||
| ⟨{ right := single (V.index), hom := V.hom_to_index }⟩ | |||
|
|
|||
| -- this is crazy crazy slow | |||
There was a problem hiding this comment.
I just spent a while removing _s to find out why the elaborator was taking 6 seconds on my machine. My tentative conclusion: left := 𝟙 _ occurs 12 times in the proof and each time the underscore, which is at least sometimes a term of type category_theory.discrete punit , is being filled in by an autoparam obviously which takes 400ms and (thanks show_term!) is producing a huge term (takes 40 lines to display).
There was a problem hiding this comment.
Nope, this isn't it :-( Here is an _-free proof, and it still takes forever:
instance : cofinal (pairwise_to_opens_le_cover U) :=
λ V, is_connected_of_zigzag (λ A B,
begin
rcases A with ⟨⟨⟩, ⟨i⟩|⟨i,j⟩, a⟩;
rcases B with ⟨⟨⟩, ⟨i'⟩|⟨i',j'⟩, b⟩;
dsimp at *,
{ exact ⟨([
{ left := punit.star, right := pair i i',
hom := hom_of_le (le_inf (le_of_hom a) (le_of_hom b)), }, {left := punit.star, right := single i', hom := b}] :
list (comma (functor.from_punit V) (pairwise_to_opens_le_cover U))),
list.chain.cons (or.inr ⟨{ left := 𝟙 (by fsplit), right := left i i', }⟩)
(list.chain.cons (or.inl ⟨{ left := 𝟙 (by fsplit), right := right i i', }⟩) list.chain.nil),
rfl⟩ },
{ exact ⟨([
{ left := punit.star, right := pair i' i,
hom := hom_of_le (le_inf ((le_of_hom b).trans inf_le_left) (le_of_hom a)), },
{ left := punit.star, right := single i',
hom := hom_of_le ((le_of_hom b).trans inf_le_left), }, {left := punit.star, right := pair i' j', hom := b}] : list (comma (functor.from_punit V) (pairwise_to_opens_le_cover U))),
list.chain.cons (or.inr ⟨{ left := 𝟙 (by fsplit), right := right i' i, }⟩)
(list.chain.cons (or.inl ⟨{ left := 𝟙 (by fsplit), right := left i' i, }⟩)
(list.chain.cons (or.inr ⟨{ left := 𝟙 (by fsplit), right := left i' j', }⟩) list.chain.nil)),
rfl⟩ },
{ exact ⟨([
{ left := punit.star, right := single i,
hom := hom_of_le ((le_of_hom a).trans inf_le_left), },
{ left := punit.star, right := pair i i', hom :=
hom_of_le (le_inf ((le_of_hom a).trans inf_le_left) (le_of_hom b)), }, {left := punit.star, right := single i', hom := b}] : list (comma (functor.from_punit V) (pairwise_to_opens_le_cover U))),
list.chain.cons (or.inl ⟨{ left := 𝟙 (by fsplit), right := left i j, }⟩)
(list.chain.cons (or.inr ⟨{ left := 𝟙 (by fsplit), right := left i i', }⟩)
(list.chain.cons (or.inl ⟨{ left := 𝟙 (by fsplit), right := right i i', }⟩) list.chain.nil)),
rfl⟩ },
{ exact ⟨([
{ left := punit.star, right := single i,
hom := hom_of_le ((le_of_hom a).trans inf_le_left), },
{ left := punit.star, right := pair i i',
hom :=
hom_of_le (le_inf ((le_of_hom a).trans inf_le_left) ((le_of_hom b).trans inf_le_left)), },
{ left := punit.star, right := single i',
hom := hom_of_le ((le_of_hom b).trans inf_le_left), }, {left := punit.star, right := pair i' j', hom := b}] : list (comma (functor.from_punit V) (pairwise_to_opens_le_cover U))),
list.chain.cons (or.inl ⟨{ left := 𝟙 (by fsplit), right := left i j, }⟩)
(list.chain.cons (or.inr ⟨{ left := 𝟙 (by fsplit), right := left i i', }⟩)
(list.chain.cons (or.inl ⟨{ left := 𝟙 (by fsplit), right := right i i', }⟩)
(list.chain.cons (or.inr ⟨{ left := 𝟙 (by fsplit), right := left i' j', }⟩) list.chain.nil))),
rfl⟩ },
end)Profiler says
elaboration: tactic execution took 5.93s
num. allocated objects: 4922
num. allocated closures: 12673
5934ms 100.0% _interaction._lambda_2
5934ms 100.0% scope_trace
5934ms 100.0% tactic.step
5934ms 100.0% _interaction
5934ms 100.0% tactic.istep._lambda_1
5934ms 100.0% tactic.istep
5872ms 99.0% tactic.solve1
5871ms 98.9% tactic.interactive.exact
5870ms 98.9% tactic.to_expr
2551ms 43.0% _interaction._lambda_6
1469ms 24.8% _interaction._lambda_4
1446ms 24.4% _interaction._lambda_5
405ms 6.8% _interaction._lambda_3
62ms 1.0% tactic.seq'
60ms 1.0% interaction_monad.monad._lambda_9
59ms 1.0% all_goals'_core
59ms 1.0% tactic.all_goals'
59ms 1.0% _private.4125604415.all_goals'_core._main._lambda_2
55ms 0.9% tactic.interactive.dsimp
...
There was a problem hiding this comment.
I can't get to the bottom of this. Each of the exacts is taking over 1 second.
instance : cofinal (pairwise_to_opens_le_cover U) :=
λ V, is_connected_of_zigzag (λ A B,
begin
rcases A with ⟨⟨⟩, ⟨i⟩|⟨i,j⟩, a⟩;
rcases B with ⟨⟨⟩, ⟨i'⟩|⟨i',j'⟩, b⟩;
dsimp at a b,
{ exact ⟨[
{ left := punit.star, right := pair i i',
hom := hom_of_le (le_inf (le_of_hom a) (le_of_hom b)), },
{left := punit.star, right := single i', hom := b}],
list.chain.cons (or.inr ⟨{ left := 𝟙 punit.star, right := left i i', w' := rfl}⟩)
(list.chain.cons (or.inl ⟨{ left := 𝟙 punit.star, right := right i i', w' := rfl}⟩)
list.chain.nil),
rfl⟩, },
{ exact ⟨[
{ left := punit.star, right := pair i' i,
hom := hom_of_le (le_inf ((le_of_hom b).trans inf_le_left) (le_of_hom a)), },
{ left := punit.star, right := single i',
hom := hom_of_le ((le_of_hom b).trans inf_le_left), },
{left := punit.star, right := pair i' j', hom := b}],
list.chain.cons (or.inr ⟨{ left := 𝟙 punit.star, right := right i' i, w' := rfl}⟩)
(list.chain.cons (or.inl ⟨{ left := 𝟙 punit.star, right := left i' i, w' := rfl}⟩)
(list.chain.cons (or.inr ⟨{ left := 𝟙 punit.star, right := left i' j', w' := rfl}⟩)
list.chain.nil)),
rfl⟩ },
{ exact ⟨[
{ left := punit.star, right := single i,
hom := hom_of_le ((le_of_hom a).trans inf_le_left), },
{ left := punit.star, right := pair i i', hom :=
hom_of_le (le_inf ((le_of_hom a).trans inf_le_left) (le_of_hom b)), },
{left := punit.star, right := single i', hom := b}],
list.chain.cons (or.inl ⟨{ left := 𝟙 punit.star, right := left i j, w' := rfl}⟩)
(list.chain.cons (or.inr ⟨{ left := 𝟙 punit.star, right := left i i', w' := rfl}⟩)
(list.chain.cons (or.inl ⟨{ left := 𝟙 punit.star, right := right i i', w' := rfl}⟩)
list.chain.nil)),
rfl⟩ },
{ exact ⟨[
{ left := punit.star, right := single i,
hom := hom_of_le ((le_of_hom a).trans inf_le_left), },
{ left := punit.star, right := pair i i',
hom :=
hom_of_le (le_inf ((le_of_hom a).trans inf_le_left) ((le_of_hom b).trans inf_le_left)), },
{ left := punit.star, right := single i',
hom := hom_of_le ((le_of_hom b).trans inf_le_left), },
{left := punit.star, right := pair i' j', hom := b}],
list.chain.cons (or.inl ⟨{ left := 𝟙 punit.star, right := left i j, w' := rfl}⟩)
(list.chain.cons (or.inr ⟨{ left := 𝟙 punit.star, right := left i i', w' := rfl}⟩)
(list.chain.cons (or.inl ⟨{ left := 𝟙 punit.star, right := right i i', w' := rfl}⟩)
(list.chain.cons (or.inr ⟨{ left := 𝟙 punit.star, right := left i' j', w' := rfl}⟩)
list.chain.nil))),
rfl⟩ },
end)I think I've filled in all the autoparams.
There was a problem hiding this comment.
Right... it's a pretty wild proof!
There was a problem hiding this comment.
The culprit is a huge type class search for a preorder instance in the first structure in the list at the beginning of each exact.
This is an extract_goal from the first of your four exact statements. 430ms with the haveI commented, 30ms with it uncommented:
example {X : Top} {ι : Type v}
(U : ι → opens ↥X)
(V : opens_le_cover U)
(i i' : ι)
(b : V ⟶ (⟨U i', _⟩ : {V // ∃ (i : ι), V ≤ U i}))
(a : V ⟶ (⟨U i, _⟩ : {V // ∃ (i : ι), V ≤ U i})) :
∃ (l : list (comma (functor.from_punit V) (pairwise_to_opens_le_cover U))),
list.chain zag ({left := punit.star, right := single i, hom := a} : comma (functor.from_punit V) (pairwise_to_opens_le_cover U)) l ∧
(({left := punit.star, right := single i, hom := a} : comma (functor.from_punit V) (pairwise_to_opens_le_cover U)) :: l).last sorry =
{left := punit.star, right := single i', hom := b} :=
begin
refine ⟨[_, _], _, _⟩,
{
refine_struct { left := punit.star, right := pair i i', },
-- haveI : preorder (@opens_le_cover X ι U) := sorry,
refine hom_of_le _, -- this is the slow bit
sorry
},
{ exact {left := punit.star, right := single i', hom := b} },
{ exact list.chain.cons (or.inr ⟨{ left := 𝟙 punit.star, right := left i i', w' := rfl}⟩)
(list.chain.cons (or.inl ⟨{ left := 𝟙 punit.star, right := right i i', w' := rfl}⟩)
list.chain.nil) },
{ refl }
end There was a problem hiding this comment.
Oh this refine ⟨[_, _], _, _⟩, is a really nice trick! Thanks!
|
@jcommelin @kbuzzard are you planning to investigate more or is this done for now? |
|
I don't have time to dive into this atm. |
|
I'm going to merge this now, to take advantage of the first pass speedup. I can't debug the slow search without understanding what's going on in the proof. It's not clear to me why the proof succeeds with this search failing. I'm also not sure why the failure isn't cached, since the context is the same at all search points and the cache is never reset. |
|
bors merge |
github-actions
bot
added
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Nov 4, 2020
…4832) There are still a bunch of things that take 10-15s on my machine. But I don't see easy ways to speed them up. (In total, these three files took up multiple minutes to compile, and it's still not great.) Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
|
Build failed (retrying...): |
bors bot
pushed a commit
that referenced
this pull request
Nov 4, 2020
…4832) There are still a bunch of things that take 10-15s on my machine. But I don't see easy ways to speed them up. (In total, these three files took up multiple minutes to compile, and it's still not great.) Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
|
Build failed: |
robertylewis
added
awaiting-author
|
Cancel that, the build is failing now. |
|
@jcommelin is this still an issue? On a recent master Is it possible this issue disappeared with other changes? |
|
@robertylewis Ooh, that's great news. Let's close this then. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There are still a bunch of things that take 10-15s on my machine.
But I don't see easy ways to speed them up.
(In total, these three files took up multiple minutes to compile,
and it's still not great.)