error: Error: tag for constructor 'ast.ZIMOP_MOP_RR' is too big, this is a limitation of the current runtime

Prerequisites

Please put an X between the brackets as you perform the following steps:

• 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

When compiling https://github.com/opencompl/sail-riscv-lean-executable with the latest lean nightly 2025-06-21, I get the error:

error: LeanRV64DExecutable/RiscvInstsEnd.lean:4057:4: failed to compile definition, compiler IR check failed at 'LeanRV64DExecutable.Functions.encdec_backwards'. Error: tag for constructor 'ast.ZIMOP_MOP_RR' is too big, this is a limitation of the current runtime
error: LeanRV64DExecutable/RiscvInstsEnd.lean:32240:4: failed to compile definition, compiler IR check failed at 'LeanRV64DExecutable.Functions.encdec_backwards_matches'. Error: depends on declaration 'LeanRV64DExecutable.Functions.encdec_backwards._closed_0', which has no executable code; consider marking definition as 'noncomputable'
error: LeanRV64DExecutable/RiscvInstsEnd.lean:58021:4: failed to compile definition, compiler IR check failed at 'LeanRV64DExecutable.Functions.encdec_compressed_backwards'. Error: tag for constructor 'ast.ZCMOP' is too big, this is a limitation of the current runtime
error: LeanRV64DExecutable/RiscvInstsEnd.lean:60965:4: failed to compile definition, compiler IR check failed at 'LeanRV64DExecutable.Functions.encdec_compressed_backwards_matches._lam_4'. Error: depends on declaration 'LeanRV64DExecutable.Functions.encdec_backwards_matches._lam_1._closed_0', which has no executable code; consider marking definition as 'noncomputable'
error: Lean exited with code 1
Some required builds logged failures:
- LeanRV64DExecutable.RiscvInstsEnd
error: build failed

Context

I chatted with @nomeata a week ago. He suggested reporting a bug. I have not yet created a minimal test case, as the machine-generated code comprises 100,000 lines, and I am unsure how to generate a synthetic reproducer manually. For the same reason, I did not test this online. Yet, I assume that would be possible based on the error for someone who knows the compiler. While we can try to create smaller inductives, it seems Lean should nevertheless not error out.

Steps to Reproduce

1. git clone https://github.com/opencompl/sail-riscv-lean-executable
2. Lake build (and wait 6 hours)

Expected behavior:

The compilation should terminate without error.

*Actual behavior:

Error: tag for constructor 'ast.ZCMOP' is too big, this is a limitation of the current runtime

Versions

Lean nightly 2025-05-21

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.