feat(frontends/lean/decl_cmds): reject unnecessary "noncomputable" annotations

library/data/real/complete.lean

@@ -218,7 +218,7 @@ theorem rewrite_helper10 (a b c d : ℝ) : c - d = (c - a) + (a - b) + (b - d) :
 
 noncomputable definition rep (x : ℝ) : s.reg_seq := some (quot.exists_rep x)
 
-noncomputable definition re_abs (x : ℝ) : ℝ :=
+definition re_abs (x : ℝ) : ℝ :=
   quot.lift_on x (λ a, quot.mk (s.r_abs a)) (take a b Hab, quot.sound (s.r_abs_well_defined Hab))
 
 theorem r_abs_nonneg {x : ℝ} : zero ≤ x → re_abs x = x :=

src/frontends/lean/decl_cmds.cpp

@@ -873,9 +873,13 @@ class definition_cmd_fn {
                     throw exception(sstream() << "definition '" << n << "' was marked as noncomputable because '" << *reason
                                     << "' is still in theorem queue (solution: use command 'reveal " << *reason << "'");
                 } else {
-                    throw exception(sstream() << "definition '" << n << "' is noncomputable, it depends on '" << *reason << "'");
+                    throw exception(sstream() << "definition '" << n
+                                    << "' is noncomputable, it depends on '" << *reason << "'");
                 }
             }
+            if (m_is_noncomputable && !is_marked_noncomputable(m_env, real_n)) {
+                throw exception(sstream() << "definition '" << n << "' was incorrectly marked as noncomputable");
+            }
             // TODO(Leo): register aux_decls
             if (!m_is_private)
                 m_p.add_decl_index(real_n, m_pos, m_p.get_cmd_token(), type);

tests/lean/noncomp_error.lean

@@ -0,0 +1 @@
+noncomputable definition a := 2

tests/lean/noncomp_error.lean.expected.out

@@ -0,0 +1 @@
+noncomp_error.lean:1:0: error: definition 'a' was incorrectly marked as noncomputable