michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(build): add IGNORE_SORRY cmake option

Browse source 
It allows us to perform nightly builds and avoid distracting warning
messages on CDASH.
This commit is contained in:
Leonardo de Moura 2014-09-26 08:55:54 -07:00
parent f05bb9daeb
commit 480bc639ea
5 changed files with 22 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
.travis.osx.yml
View file

@ -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:

2
.travis.windows.yml
View file

@ -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;

2
.travis.yml
View file

@ -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

9
src/CMakeLists.txt
View file

@ -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"))

10
src/frontends/lean/parser.cpp
View file

@ -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([&]() {