Olean problem (I think)

Stream: new members

[Aaron Anderson]

On branch finsupp_lattice PR #3335, I keep getting catastrophic failure where everything seems to be importing twice, such as this:

excessive memory consumption detected at 'replace' (potential solution: increase memory consumption threshold)```

[Aaron Anderson]

I think it's a problem with the oleans, but it persists every time I redownload, and none of the leanproject commands I've tried has helped me.

[Aaron Anderson]

@Scott Morrison

[Scott Morrison]

Can you try leanproject -f up?

[Scott Morrison]

That should successfully retrieve something from https://oleanstorage.azureedge.net/mathlib/41dfff7c8c553ef9ab92b1f4b3c674030ee440f5.tar.xz

[Scott Morrison]

After which

$ leanproject build
Building project mathlib
configuring mathlib 0.1
> lean --make src
/Users/scott/projects/lean/mathlib/src/data/finsupp/lattice.lean:78:28: error: type mismatch at application
  support_inf_of_non_disjoint zero_le
term
  zero_le
has type
  ∀ (a : ?m_1), 0 ≤ a
but is expected to have type
  ∀ (x : ?m_1), 0 ≤ x
state:
α : Type u_1,
γ : Type u_4,
_inst_3 : canonically_linear_ordered_add_monoid γ,
f g : α →₀ γ
⊢ (semilattice_inf.inf f g).support = f.support ∩ g.support
external command exited with status 1
Command '['leanpkg', 'build']' returned non-zero exit status 1.

[Scott Morrison]

should just take a few seconds.

[Aaron Anderson]

Looks all good, thanks!