From 9bcfc06bd04b44e5cc8beaf00050cef717a46b83 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Fri, 24 Feb 2017 14:46:47 +0100 Subject: [PATCH] fix(library/module): has_sorry: check examples --- src/library/module.cpp | 4 +++- tests/lean/1369.lean.expected.out | 3 +++ tests/lean/anc1.lean.expected.out | 1 + tests/lean/bad_error2.lean.expected.out | 1 + tests/lean/error_pos.lean.expected.out | 1 + tests/lean/quot_bug.lean.expected.out | 1 + tests/lean/vm_sorry.lean.expected.out | 3 +++ 7 files changed, 13 insertions(+), 1 deletion(-) diff --git a/src/library/module.cpp b/src/library/module.cpp index 86537ec4b9..b527f4b043 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -444,8 +444,10 @@ struct add_decl_sorry_check : public task { return optional(); if (!is_internal_name(n)) return optional(n); - if (!n.is_string() || n.is_atomic()) + if (!n.is_string()) return optional(); + if (strcmp(n.get_string(), "_example") == 0) + return optional(n); if (strcmp(n.get_string(), "_main") == 0) return should_report_sorry(n.get_prefix()); if (strncmp(n.get_string(), "_match", 6) == 0) { diff --git a/tests/lean/1369.lean.expected.out b/tests/lean/1369.lean.expected.out index cab9fe1f33..001d5b1df2 100644 --- a/tests/lean/1369.lean.expected.out +++ b/tests/lean/1369.lean.expected.out @@ -1,4 +1,7 @@ +1369.lean:15:8: warning: declaration '_example' uses sorry 17 ≤ 555555 ⊢ 17 ≤ 555555 +1369.lean:21:8: warning: declaration '_example' uses sorry ?m_1 ≤ 555555 ⊢ ?m_1 ≤ 555555 +1369.lean:33:8: warning: declaration '_example' uses sorry diff --git a/tests/lean/anc1.lean.expected.out b/tests/lean/anc1.lean.expected.out index 946d899075..888bdd949f 100644 --- a/tests/lean/anc1.lean.expected.out +++ b/tests/lean/anc1.lean.expected.out @@ -1,5 +1,6 @@ (1, 2) : ℕ × ℕ and.intro trivial trivial : true ∧ true +anc1.lean:5:8: warning: declaration '_example' uses sorry {fst := 1, snd := sorry} : Σ' (x : ℕ), x > 0 show true, from true.intro : true Exists.intro 1 (id_locked (1 ≠ 0) (λ (a : 1 = 0), nat.no_confusion a)) : ∃ (x : ℕ), 1 ≠ 0 diff --git a/tests/lean/bad_error2.lean.expected.out b/tests/lean/bad_error2.lean.expected.out index 838f3039fa..4c40faaae1 100644 --- a/tests/lean/bad_error2.lean.expected.out +++ b/tests/lean/bad_error2.lean.expected.out @@ -7,3 +7,4 @@ _match : (∃ (k_1 : ℕ), k + n + k_1 = k + m) → n ≤ m, w : ℕ, hw : (λ (k_1 : ℕ), k + n + k_1 = k + m) w ⊢ n + w = m +bad_error2.lean:3:8: warning: declaration '_example' uses sorry diff --git a/tests/lean/error_pos.lean.expected.out b/tests/lean/error_pos.lean.expected.out index cc60ff69aa..65614b9b53 100644 --- a/tests/lean/error_pos.lean.expected.out +++ b/tests/lean/error_pos.lean.expected.out @@ -1,5 +1,6 @@ error_pos.lean:1:39: error: type expected at B +error_pos.lean:1:8: warning: declaration '_example' uses sorry error_pos.lean:4:43: error: type expected at B error_pos.lean:9:39: error: type expected at diff --git a/tests/lean/quot_bug.lean.expected.out b/tests/lean/quot_bug.lean.expected.out index d925317acc..d49b118ee6 100644 --- a/tests/lean/quot_bug.lean.expected.out +++ b/tests/lean/quot_bug.lean.expected.out @@ -1 +1,2 @@ λ (x : A), f x +quot_bug.lean:8:8: warning: declaration '_example' uses sorry diff --git a/tests/lean/vm_sorry.lean.expected.out b/tests/lean/vm_sorry.lean.expected.out index 45dfdfa091..29f9c7954a 100644 --- a/tests/lean/vm_sorry.lean.expected.out +++ b/tests/lean/vm_sorry.lean.expected.out @@ -3,3 +3,6 @@ vm_sorry.lean:1:4: warning: declaration 'half_baked' uses sorry vm_sorry.lean:6:0: error: half_baked._main._val_1: trying to evaluate sorry vm_sorry.lean:12:0: error: undefined (some nat) +vm_sorry.lean:18:8: warning: declaration '_example' uses sorry +vm_sorry.lean:19:8: warning: declaration '_example' uses sorry +vm_sorry.lean:20:8: warning: declaration '_example' uses sorry