[Merged by Bors] - perf: Data.Sign

[digama0]

This single file uses more than twice as much RAM as the next largest file in mathlib, see https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/mathlib4.20speedcenter/near/342595677. A simple out-lining fixes the issue.

---

[digama0]

!bench

[eric-wieser]

Any idea why? Is it unable to parallelize between fields? Does using the async tactic (if that still exist) allow it to remain inlined?

[leanprover-bot]

Here are the benchmark results for commit 529fcfa.
There were significant changes against commit 5163d8c:

  Benchmark   Metric        Change
  ================================
+ build       compilation   -10.5%
+ build       maxrss        -54.6%
- build       norm_num        6.6%

[digama0]

@eric-wieser The abstract tactic would be perfect for this but it hasn't been ported. (I have some abortive work on that tactic in a local branch.) Nothing about this is parallelized, and that's not the issue. Something about the structure of the definition triggers the old compiler to have some weird behavior, I'm not sure exactly what but it might be lifting the match statements and making 27 * 9 copies of the instance itself. It's the old compiler so it isn't likely to be fixed, hence the workaround.

[ChrisHughes24]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style