Zulip Chat Archive

Stream: new members

Topic: Olean problem (I think)


view this post on Zulip Aaron Anderson (Jul 21 2020 at 23:30):

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)```

view this post on Zulip Aaron Anderson (Jul 21 2020 at 23:32):

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.

view this post on Zulip Aaron Anderson (Jul 22 2020 at 00:00):

@Scott Morrison

view this post on Zulip Scott Morrison (Jul 22 2020 at 00:01):

Can you try leanproject -f up?

view this post on Zulip Scott Morrison (Jul 22 2020 at 00:02):

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

view this post on Zulip Scott Morrison (Jul 22 2020 at 00:02):

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.

view this post on Zulip Scott Morrison (Jul 22 2020 at 00:03):

should just take a few seconds.

view this post on Zulip Aaron Anderson (Jul 22 2020 at 00:04):

Looks all good, thanks!


Last updated: May 13 2021 at 16:25 UTC