Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

is_bi_equal use of BinderInfo-unaware hashes causes many collisions (a.k.a. timeout when saving oleans) #749

Open
1 task done
collares opened this issue Jul 29, 2022 · 0 comments

Comments

@collares
Copy link

collares commented Jul 29, 2022

Prerequisites

  • Put an X between the brackets on this line if you have done all of the following:
    • Checked that your issue isn't already filed.
    • Reduced the issue to a self-contained, reproducible test case.

Description

@digama0's testcase from https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.22saving.20olean.22.3F, reproduced below, fails to produce oleans with lean --make -T100000 test.lean:

import algebra.field.basic
import algebra.order.ring

set_option old_structure_cmd true

class linear_ordered_semifield (α : Type*)
  extends linear_ordered_semiring α, semifield α

class linear_ordered_field (α : Type*) extends linear_ordered_comm_ring α, field α

I investigated the problem a bit and found out that serializing those objects involves a lot of comparisons which increment the heartbeat counter. In particular, a lot of time is spent comparing deep expressions for BinderInfo-aware equality; the expression hash used in the comparison does not include BinderInfo data, and the above example seems to involve expressions which all have the same hash despite being different for the purposes of is_bi_equal.

Since there are only two comparison modes, a possible fix would be to have two hashes, one for each choice of CompareBinderInfo. I can't tell if this is worth the extra time and memory.

(Note: The above example may hit #748 on a debug build. Those issues may or may not be related.)

Steps to Reproduce

  1. Run lean --make -T100000 test.lean on the above file

Expected behavior: Valid oleans should be output

Actual behavior: Empty oleans

Reproduces how often: 100%

Versions

Lean (version 3.45.0, commit 22b09be, Release)

bors bot pushed a commit to leanprover-community/mathlib3 that referenced this issue Aug 31, 2022
We are currently experiencing timeouts when saving some oleans (leanprover-community/lean#749). Since Lean does not error out when deterministic timeouts happen during olean generation (leanprover-community/lean#750) and we already run Lean twice when compiling mathlib, Ben Toner suggested the following clever hack: Increase the timeout, but only on the second lean run. This effectively means anything that was reported as a timeout before is still reported as a timeout (by the first call), while olean generation gets more heartbeats.

Co-authored-by: Ben Toner <bentoner@bentoner.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant