Compilation of large inductive type definition takes ~20mins

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Consider the following Lean 4 source files: src.zip

• Sorts.lean contains a large mutual block of circular inductive and structure declarations.
• Rewrite.lean contains an even larger dependent inductive type declaration.

On my system, Sorts.lean takes 2 mins, and Rewrite.lean takes 20 mins to compile, and both require setting maxHeartbeats to a large number. I'd like to confirm whether these compilation times are expected for definitions of this complexity, or something that indicate a bug or inefficiency in the compiler.

Context

The source files have been auto-generated from KEVM, the K Framework definition of the EVM.

Steps to Reproduce

Download source, unzip, then make.

Versions

Lean version: 4.16.0-nightly-2025-01-28

OS version: 22.04.5 LTS (Jammy Jellyfish)

Download and unzip src.zip, then inspect Sorts.lean and Rewrite.lean, focusing on the large mutual and dependent inductive declarations. Run make with the reported Lean nightly version and compare compilation times and heartbeat requirements. Done means determining whether the behavior is expected for these definitions or identifying a compiler inefficiency to investigate.