building mathlib

Stream: maths

[Sean Leather]

I'm trying to build the mathlib master with the Lean master. Should this work? I currently get this as the first error (followed by others):

mathlib/data/finset.lean:846:12: error: rewrite tactic failed, did not find instance of the pattern in the target expression
  ?m_2 ∈ multiset.to_finset ?m_4
state:
α : Type u_1,
δ : α → Type u_4,
_inst_1 : decidable_eq α,
_inst_2 : Π (a : α), decidable_eq (δ a),
t : Π (a : α), finset (δ a),
s_val : multiset α,
s_nodup : multiset.nodup s_val,
f : Π (a : α), a ∈ {val := s_val, nodup := s_nodup} → δ a
⊢ f ∈ multiset.to_finset (multiset.pi ({val := s_val, nodup := s_nodup}.val) (λ (a : α), (t a).val)) ↔
    ∀ (a : α) (h : a ∈ {val := s_val, nodup := s_nodup}), f a h ∈ t a

[Mario Carneiro]

mathlib is currently building against nightly 04-06. I've been waiting for the 3.4.0 nightly to be released, which happened yesterday; I'll take a look at updating later.

[Sean Leather]

Yay! I can build lean and mathlib. :person_doing_cartwheel: Thanks, @Mario Carneiro!

[Sean Leather]

Wow! I just upgraded my Lean and mathlib from February to the latest, and I didn't have to change a thing in my code. :astonished:

[Mario Carneiro]

that must be a record, two months without a backward incompatibility