From 480bc639ea97529ba15c52d86ba5d9f2758c2095 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 26 Sep 2014 08:55:54 -0700
Subject: [PATCH] feat(build): add IGNORE_SORRY cmake option

It allows us to perform nightly builds and avoid distracting warning
messages on CDASH.
---
 .travis.osx.yml               |  2 +-
 .travis.windows.yml           |  2 +-
 .travis.yml                   |  2 +-
 src/CMakeLists.txt            |  9 +++++++++
 src/frontends/lean/parser.cpp | 10 ++++++++++
 5 files changed, 22 insertions(+), 3 deletions(-)

diff --git a/.travis.osx.yml b/.travis.osx.yml
index 3757ab9e7..622e10d4d 100644
--- a/.travis.osx.yml
+++ b/.travis.osx.yml
@@ -49,7 +49,7 @@ install:
 before_script:
 - mkdir -p build
 - cd build
-- cmake -DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE} -DTCMALLOC=${TCMALLOC} -DMULTI_THREAD=${MULTI_THREAD} -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} ../src -G Ninja
+- cmake -DIGNORE_SORRY=ON -DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE} -DTCMALLOC=${TCMALLOC} -DMULTI_THREAD=${MULTI_THREAD} -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} ../src -G Ninja
 - cd ..
 
 # Remark:
diff --git a/.travis.windows.yml b/.travis.windows.yml
index a6b3e68d9..aafd3e3cb 100644
--- a/.travis.windows.yml
+++ b/.travis.windows.yml
@@ -24,7 +24,7 @@ script:
   - mkdir -p build
   - LEAN_ROOT=`pwd`
   - cd build
-  - cmake -DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE} ../src -DTCMALLOC=OFF -DCMAKE_TOOLCHAIN_FILE=/tmp/mxe/usr/x86_64-w64-mingw32/share/cmake/mxe-conf.cmake
+  - cmake -DIGNORE_SORRY=ON -DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE} ../src -DTCMALLOC=OFF -DCMAKE_TOOLCHAIN_FILE=/tmp/mxe/usr/x86_64-w64-mingw32/share/cmake/mxe-conf.cmake
   - SITE=Windows@Travis
   - if [[ $CMAKE_BUILD_TYPE == RELEASE ]]; then
         BUILD_TYPE=Release;
diff --git a/.travis.yml b/.travis.yml
index 364b58079..1332b98e6 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -230,7 +230,7 @@ script:
   - if [[ $TESTCOV != ON ]]; then
        TESTCOV=OFF;
     fi
-  - /usr/bin/cmake -DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE} -DTESTCOV=${TESTCOV} -DTCMALLOC=${TCMALLOC} -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} ${GENERATOR} -DCMAKE_PROGRAM_PATH=/usr/bin ../src;
+  - /usr/bin/cmake -DIGNORE_SORRY=ON -DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE} -DTESTCOV=${TESTCOV} -DTCMALLOC=${TCMALLOC} -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} ${GENERATOR} -DCMAKE_PROGRAM_PATH=/usr/bin ../src;
   - if [[ $CMAKE_BUILD_TYPE == DEBUG || $CMAKE_BUILD_TYPE == RELEASE || $TESTCOV == ON ]]; then
        SITE=Ubuntu12.04@Travis;
        if [[ $CMAKE_BUILD_TYPE == RELEASE ]]; then
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 7c3ce4ccb..f78b81f11 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -20,6 +20,10 @@ option(READLINE           "READLINE"           OFF)
 option(CACHE_EXPRS        "CACHE_EXPRS"        ON)
 option(TCMALLOC           "TCMALLOC"           ON)
 option(JEMALLOC           "JEMALLOC"           OFF)
+# IGNORE_SORRY is a tempory option (hack). It allows us to build
+# a version of Lean that does not report when 'sorry' is used.
+# This is useful for suppressing warning messages in the nightly builds.
+option(IGNORE_SORRY       "IGNORE_SORRY"      OFF)
 
 # Added for CTest
 include(CTest)
@@ -72,6 +76,11 @@ set(CMAKE_CXX_FLAGS_GPROF          "-O2 -g -pg")
 include(CheckIncludeFileCXX)
 check_include_file_cxx("unistd.h" HAVE_UNISTD)
 
+if ("${IGNORE_SORRY}" MATCHES "ON")
+  message(STATUS "IGNORE_SORRY is ON, Lean will not report when 'sorry' is used directly or indirectly")
+  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -D LEAN_IGNORE_SORRY")
+endif()
+
 # SPLIT_STACK
 if ("${SPLIT_STACK}" MATCHES "ON")
   if ((${CMAKE_SYSTEM_NAME} MATCHES "Linux") AND ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU"))
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index db9f6f928..225efd81d 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -157,9 +157,14 @@ bool parser::are_info_lines_valid(unsigned start_line, unsigned end_line) const
 expr parser::mk_sorry(pos_info const & p) {
     m_used_sorry = true;
     {
+#ifndef LEAN_IGNORE_SORRY
+        // TODO(Leo): remove the #ifdef.
+        // The compilation option LEAN_IGNORE_SORRY is a temporary hack for the nightly builds
+        // We use it to avoid a buch of warnings on cdash.
         flycheck_warning wrn(regular_stream());
         display_warning_pos(p.first, p.second);
         regular_stream() << " using 'sorry'" << endl;
+#endif
     }
     return save_pos(::lean::mk_sorry(), p);
 }
@@ -1259,9 +1264,14 @@ bool parser::parse_commands() {
             },
             [&]() { sync_command(); });
         if (has_sorry(m_env)) {
+#ifndef LEAN_IGNORE_SORRY
+            // TODO(Leo): remove the #ifdef.
+            // The compilation option LEAN_IGNORE_SORRY is a temporary hack for the nightly builds
+            // We use it to avoid a buch of warnings on cdash.
             flycheck_warning wrn(regular_stream());
             display_warning_pos(pos());
             regular_stream() << " imported file uses 'sorry'" << endl;
+#endif
         }
         while (!done) {
             protected_call([&]() {