Consider marking it as 'noncomputable' (Lean 4)
Lean tried to compile your definition into runnable code, but it uses something that only exists logically — such as Classical.choose or a noncomputable Mathlib definition.
What it looks like
Main.lean:4:4: error(lean.dependsOnNoncomputable): failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Classical.choose', which is 'noncomputable'What does "Consider marking it as 'noncomputable' (Lean 4)" mean?
Lean compiles every def so it can be run with #eval, unless you say otherwise. Logic-only ingredients such as Classical.choice have no code, so compilation fails and Lean suggests noncomputable. Since Lean 4.22, where the new code generator became the default, the message ends which is 'noncomputable' and the command line labels it error(lean.dependsOnNoncomputable); Lean 4.21 and earlier often printed … because it depends on 'X', and it does not have executable code. An axiom used as data is reported as `X` not supported by code generator; consider marking definition as `noncomputable`.
What causes "Consider marking it as 'noncomputable' (Lean 4)"?
- The definition uses classical choice: Classical.choose, Classical.choice, or an if on a proposition that is only decidable via open Classical.
- It calls a Mathlib definition that is already marked noncomputable (much of the real-number API, for example).
- It uses an axiom or a theorem as if it were data.
How do I confirm the cause?
- The name after depends on is the culprit; check whether it is something you actually need at run time.
- Run #print axioms on the definition — Classical.choice in the list shows that classical reasoning came in somewhere.
How do I fix "Consider marking it as 'noncomputable' (Lean 4)"?
- Mark it noncomputable def (or noncomputable instance) — fine when you only use it in proofs.
- Put noncomputable section at the top of the file or section so everything inside is allowed to be noncomputable.
- If you need to run it, replace the classical part with a computable one — a real Decidable instance instead of open Classical, or an explicit search instead of Classical.choose.
How do I stop it happening again?
- Use noncomputable section in files of pure mathematics where nothing needs to run.
- Keep code you want to #eval separate from classical definitions used only in proofs.