From 69ead0ddd877c4efd2c35287c6c245fdfece8b67 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 29 Jul 2015 08:28:40 -0700 Subject: [PATCH] feat(frontends/lean/decl_cmds): reject unnecessary "noncomputable" annotations --- library/data/real/complete.lean | 2 +- src/frontends/lean/decl_cmds.cpp | 6 +++++- tests/lean/noncomp_error.lean | 1 + tests/lean/noncomp_error.lean.expected.out | 1 + 4 files changed, 8 insertions(+), 2 deletions(-) create mode 100644 tests/lean/noncomp_error.lean create mode 100644 tests/lean/noncomp_error.lean.expected.out diff --git a/library/data/real/complete.lean b/library/data/real/complete.lean index 2bff36f60..45b31c62a 100644 --- a/library/data/real/complete.lean +++ b/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 := diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 9fe4aab49..b0c57af82 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/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); diff --git a/tests/lean/noncomp_error.lean b/tests/lean/noncomp_error.lean new file mode 100644 index 000000000..8f49f6777 --- /dev/null +++ b/tests/lean/noncomp_error.lean @@ -0,0 +1 @@ +noncomputable definition a := 2 diff --git a/tests/lean/noncomp_error.lean.expected.out b/tests/lean/noncomp_error.lean.expected.out new file mode 100644 index 000000000..15d3c3dd0 --- /dev/null +++ b/tests/lean/noncomp_error.lean.expected.out @@ -0,0 +1 @@ +noncomp_error.lean:1:0: error: definition 'a' was incorrectly marked as noncomputable