Zulip Chat Archive

Stream: general

Topic: getting PRs merged

Johan Commelin (Dec 17 2018 at 13:12):

@Mario Carneiro @Johannes Hölzl Is there anything we can do so that a bunch of PRs get merged before the Christmas break? Merging these PRs would mean that we can spend our Christmas holidays on interesting maths stuff, instead of boring parties with food and fire crackers...

Johan Commelin (Dec 17 2018 at 14:17):

Yuchai! We're down to 29!

Kenny Lau (Dec 17 2018 at 14:20):

:o

Mario Carneiro (Dec 17 2018 at 14:21):

...and now mathlib is broken

Kenny Lau (Dec 17 2018 at 14:21):

:o

Mario Carneiro (Dec 17 2018 at 14:23):

oh, I think it was the squeeze_simp PR

Mario Carneiro (Dec 17 2018 at 14:23):

@Johan Commelin did you actually check that your import works?

Johan Commelin (Dec 17 2018 at 14:24):

Hmm, it looked like it, but I didn't do a full compile.

Johan Commelin (Dec 17 2018 at 14:24):

Can you revert that commit?

Johan Commelin (Dec 17 2018 at 14:24):

Then I will do a more careful check.

Johan Commelin (Dec 17 2018 at 14:24):

Sorry for the mess.

Chris Hughes (Dec 17 2018 at 14:25):

I think it's a cyclic import

Chris Hughes (Dec 17 2018 at 14:25):

Maybe two PRs added imports somewhere

Mario Carneiro (Dec 17 2018 at 14:27):

tactic.squeeze imports meta.rb_map which imports data.option which imports tactic.interactive

Kenny Lau (Dec 17 2018 at 14:27):

where's the cycle?

Chris Hughes (Dec 17 2018 at 14:28):

tactic.interactive imports tactic.squeeze

Kenny Lau (Dec 17 2018 at 14:28):

why would it...

Johan Commelin (Dec 17 2018 at 14:30):

Because then it makes it a lot easier for mere mortals to squeeze their simps. Would save you a lot of work.

Johan Commelin (Dec 17 2018 at 14:42):

@Mario Carneiro Do you want me to PR a reverting commit?

Mario Carneiro (Dec 17 2018 at 14:42):

no, I'm working on it

Kenny Lau (Dec 17 2018 at 14:42):

thanks @Mario Carneiro

Johan Commelin (Dec 17 2018 at 14:45):

I can make data.option work without tactic.interactive, it just used two simpas

Johan Commelin (Dec 17 2018 at 14:45):

But there is another cycle.

Johan Commelin (Dec 17 2018 at 14:45):

category.traversable.instances imports -- import data.list.basic data.set.lattice

Johan Commelin (Dec 17 2018 at 14:46):

It needs those for

lemma mem_traverse {f : α' → set β'} :
  ∀(l : list α') (n : list β'), n ∈ traverse f l ↔ forall₂ (λb a, b ∈ f a) n l
| []      []      := by simp
| (a::as) []      := by simp; exact assume h, match h with end
| []      (b::bs) := by simp
| (a::as) (b::bs) :=
  suffices (b :: bs : list β') ∈ traverse f (a :: as) ↔ b ∈ f a ∧ bs ∈ traverse f as,
    by simpa [mem_traverse as bs],
  iff.intro
    (assume ⟨_, ⟨b, hb, rfl⟩, _, hl, rfl⟩, ⟨hb, hl⟩)
    (assume ⟨hb, hl⟩, ⟨_, ⟨b, hb, rfl⟩, _, hl, rfl⟩)

Johan Commelin (Dec 17 2018 at 14:46):

If we kick that to another file, it seems that the world would be happy again.

Johan Commelin (Dec 17 2018 at 14:48):

Once again, I apologize for breaking stuff. I'll take this as a lesson that I shouldn't lightly PR things that are low in the dependency chain...

Johan Commelin (Dec 17 2018 at 14:49):

Aahrg... it's even worse. tactic.squeeze depends on simpa (of course :face_palm:).

Johan Commelin (Dec 17 2018 at 17:27):

@Mario Carneiro Thanks for all the merges! And thanks for fixing what I broke. :thank_you: :thumbs_up: :tada:

Last updated: Dec 20 2023 at 11:08 UTC