GCC: ‘this’ was not captured for this lambda function

[EdAyers]

Prerequisites

• [x] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs, or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Similar issue: #1619

I am failing to build Lean on my fresh Arch Linux VM.

I am using commit ceacfa74

I followed the build instuctions on the make step, the C++ compiler returns the errors

...
In file included from /home/edward/lean/src/frontends/lean/token_table.h:10,
                 from /home/edward/lean/src/frontends/lean/scanner.h:17,
                 from /home/edward/lean/src/frontends/lean/parser_state.h:13,
                 from /home/edward/lean/src/frontends/lean/module_parser.h:14,
                 from /home/edward/lean/src/library/module_mgr.h:13,
                 from /home/edward/lean/src/library/module.cpp:31:
/home/edward/lean/src/util/trie.h: In lambda function:
/home/edward/lean/src/util/trie.h:69:76: error: ‘this’ was not captured for this lambda function
                     new_t1->m_children.insert(k, trie::merge(n1.steal(), c2));
                                                                            ^
/home/edward/lean/src/util/trie.h: In lambda function:
/home/edward/lean/src/util/trie.h:82:44: error: ‘this’ was not captured for this lambda function
                 trie::for_each(f, c, prefix);
                                            ^
/home/edward/lean/src/library/module.cpp: In function ‘void lean::import_module(lean::environment&, const string&, const lean::module_name&, const module_loader&, lean::buffer<lean::import_error>&)’:
/home/edward/lean/src/library/module.cpp:607:14: warning: catching polymorphic type ‘class lean::throwable’ by value [-Wcatch-value=]
     } catch (throwable) {
              ^~~~~~~~~
make[2]: *** [library/CMakeFiles/library.dir/build.make:180: library/CMakeFiles/library.dir/module.cpp.o] Error 1
make[1]: *** [CMakeFiles/Makefile2:1681: library/CMakeFiles/library.dir/all] Error 2
make: *** [Makefile:163: all] Error 2                         ^

I don't have enough knowledge of C++ lambdas to know why it is saying this. But the same thing happened in #1619 over a year ago and a change was made to the lean sourcecode to fix it. I am using gcc 8.1.1 It is most likely I just installed the wrong version of a tool or forgot a flag but I don't know which one.

I get the same error if I use cmake -D CMAKE_CXX_COMPILER=gcc ../../src

Output from cmake:

-- The CXX compiler identification is GNU 8.1.1
-- The C compiler identification is GNU 8.1.1
-- Check for working CXX compiler: /usr/bin/c++
-- Check for working CXX compiler: /usr/bin/c++ -- works
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- Check for working C compiler: /usr/bin/cc
-- Check for working C compiler: /usr/bin/cc -- works
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Detecting C compile features
-- Detecting C compile features - done
-- No build type selected, default to Release
-- Lean library will be installed at /usr/local/lib/lean
-- Found GMP: /usr/include (Required is at least version "5.0.5")
-- Using standard malloc.
-- Found PythonInterp: /usr/bin/python (found version "3.6.6") 
-- git commit sha1: ceacfa7445953cbc8860ddabc55407430a9ca5c3
-- Configuring done
-- Generating done
-- Build files have been written to: /home/edward/lean/build/release

Versions:

cmake version 3.11.4
gcc version 8.1.1 20180531 (GCC) 

Please let me know if you need other logs and versions.

[cipher1024]

Have you tried using ninja?

[gebner]

This error is introduced in gcc 8. There should be no problems with gcc 7.

[EdAyers]

I installed gcc7 and passed the flag -D CMAKE_CXX_COMPILER=gcc-7 to cmake and it has fixed the above error. But now I am getting a gigantic error message at the linking phase.

Scanning dependencies of target lean
[ 68%] Building CXX object shell/CMakeFiles/lean.dir/lean.cpp.o
[ 68%] Building CXX object shell/CMakeFiles/lean.dir/server.cpp.o
[ 68%] Building CXX object shell/CMakeFiles/lean.dir/leandoc.cpp.o
[ 68%] Linking CXX executable lean
CMakeFiles/lean.dir/server.cpp.o: In function `void std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >::_M_construct<char*>(char*, char*, std::forward_iterator_tag) [clone .isra.271]':
server.cpp:(.text+0xe9): undefined reference to `std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >::_M_create(unsigned long&, unsigned long)'
server.cpp:(.text+0x127): undefined reference to `std::__throw_logic_error(char const*)'
CMakeFiles/lean.dir/server.cpp.o: In function `lean::region_of_interest::intersects(lean::location const&) const':
server.cpp:(.text+0x1ab): undefined reference to `std::_Hash_bytes(void const*, unsigned long, unsigned long)'
server.cpp:(.text+0x267): undefined reference to `std::_Hash_bytes(void const*, unsigned long, unsigned long)'
server.cpp:(.text+0x390): undefined reference to `std::__throw_out_of_range(char const*)'
CMakeFiles/lean.dir/server.cpp.o: In function `lean::server_dump_log_tree()':
server.cpp:(.text+0x53a): undefined reference to `std::cerr'
CMakeFiles/lean.dir/server.cpp.o: In function `lean::server::get_roi()':
server.cpp:(.text+0x5e2): undefined reference to `std::__throw_system_error(int)'
CMakeFiles/lean.dir/server.cpp.o: In function `lean::server_print_roi()':
server.cpp:(.text+0x643): undefined reference to `std::cerr'
server.cpp:(.text+0x657): undefined reference to `std::basic_ostream<char, std::char_traits<char> >& std::__ostream_insert<char, std::char_traits<char> >(std::basic_ostream<char, std::char_traits<char> >&, char const*, long)'
server.cpp:(.text+0x662): undefined reference to `std::ostream::operator<<(int)'
server.cpp:(.text+0x693): undefined reference to `std::ostream::put(char)'
server.cpp:(.text+0x69b): undefined reference to `std::ostream::flush()'
server.cpp:(.text+0x6c4): undefined reference to `std::basic_ostream<char, std::char_traits<char> >& std::__ostream_insert<char, std::char_traits<char> >(std::basic_ostream<char, std::char_traits<char> >&, char const*, long)'
server.cpp:(.text+0x6f5): undefined reference to `std::ostream::put(char)'
server.cpp:(.text+0x6fd): undefined reference to `std::ostream::flush()'
server.cpp:(.text+0x720): undefined reference to `std::ostream::put(char)'
server.cpp:(.text+0x728): undefined reference to `std::ostream::flush()'
server.cpp:(.text+0x749): undefined reference to `std::basic_ostream<char, std::char_traits<char> >& std::__ostream_insert<char, std::char_traits<char> >(std::basic_ostream<char, std::char_traits<char> >&, char const*, long)'
server.cpp:(.text+0x753): undefined reference to `std::ostream& std::ostream::_M_insert<unsigned long>(unsigned long)'
server.cpp:(.text+0x76a): undefined reference to `std::basic_ostream<char, std::char_traits<char> >& std::__ostream_insert<char, std::char_traits<char> >(std::basic_ostream<char, std::char_traits<char> >&, char const*, long)'
server.cpp:(.text+0x775): undefined reference to `std::ostream& std::ostream::_M_insert<unsigned long>(unsigned long)'
server.cpp:(.text+0x7a2): undefined reference to `std::ctype<char>::_M_widen_init() const'
server.cpp:(.text+0x814): undefined reference to `std::ctype<char>::_M_widen_init() const'
server.cpp:(.text+0x844): undefined reference to `std::ctype<char>::_M_widen_init() const'
server.cpp:(.text+0x86f): undefined reference to `std::__throw_bad_cast()'
server.cpp:(.text+0x891): undefined reference to `std::__throw_bad_cast()'
server.cpp:(.text+0x89b): undefined reference to `std::__throw_bad_cast()'
CMakeFiles/lean.dir/server.cpp.o: In function `std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long, unsigned long, double, std::allocator>::get_impl<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, 0>(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >*) const [clone .constprop.552]':
server.cpp:(.text+0x90e): undefined reference to `__cxa_allocate_exception'
server.cpp:(.text+0x940): undefined reference to `std::domain_error::domain_error(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)'
server.cpp:(.text+0x953): undefined reference to `operator delete(void*)'
server.cpp:(.text+0x966): undefined reference to `operator delete(void*)'

... then about a megabyte of similar output...

file_lock.cpp:(.text+0x152): undefined reference to `std::basic_ostream<char, std::char_traits<char> >& std::operator<< <std::char_traits<char> >(std::basic_ostream<char, std::char_traits<char> >&, char const*)'
file_lock.cpp:(.text+0x15d): undefined reference to `std::basic_ostream<char, std::char_traits<char> >& std::operator<< <std::char_traits<char> >(std::basic_ostream<char, std::char_traits<char> >&, char const*)'
file_lock.cpp:(.text+0x16c): undefined reference to `std::basic_ostream<char, std::char_traits<char> >& std::operator<< <std::char_traits<char> >(std::basic_ostream<char, std::char_traits<char> >&, char const*)'
file_lock.cpp:(.text+0x18d): undefined reference to `std::__cxx11::basic_ostringstream<char, std::char_traits<char>, std::allocator<char> >::~basic_ostringstream()'
file_lock.cpp:(.text+0x1a3): undefined reference to `__cxa_throw'
file_lock.cpp:(.text+0x1bb): undefined reference to `std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >::_M_create(unsigned long&, unsigned long)'
file_lock.cpp:(.text+0x20d): undefined reference to `operator delete(void*)'
file_lock.cpp:(.text+0x221): undefined reference to `std::__throw_length_error(char const*)'
file_lock.cpp:(.text+0x235): undefined reference to `__cxa_allocate_exception'
file_lock.cpp:(.text+0x254): undefined reference to `std::__cxx11::basic_ostringstream<char, std::char_traits<char>, std::allocator<char> >::basic_ostringstream(std::_Ios_Openmode)'
file_lock.cpp:(.text+0x263): undefined reference to `std::basic_ostream<char, std::char_traits<char> >& std::operator<< <std::char_traits<char> >(std::basic_ostream<char, std::char_traits<char> >&, char const*)'
file_lock.cpp:(.text+0x26e): undefined reference to `std::basic_ostream<char, std::char_traits<char> >& std::operator<< <std::char_traits<char> >(std::basic_ostream<char, std::char_traits<char> >&, char const*)'
file_lock.cpp:(.text+0x27d): undefined reference to `std::basic_ostream<char, std::char_traits<char> >& std::operator<< <std::char_traits<char> >(std::basic_ostream<char, std::char_traits<char> >&, char const*)'
file_lock.cpp:(.text+0x29e): undefined reference to `std::__cxx11::basic_ostringstream<char, std::char_traits<char>, std::allocator<char> >::~basic_ostringstream()'
file_lock.cpp:(.text+0x2b4): undefined reference to `__cxa_throw'
file_lock.cpp:(.text+0x2c0): undefined reference to `std::__throw_logic_error(char const*)'
file_lock.cpp:(.text+0x2cb): undefined reference to `std::__cxx11::basic_ostringstream<char, std::char_traits<char>, std::allocator<char> >::~basic_ostringstream()'
file_lock.cpp:(.text+0x2d3): undefined reference to `__cxa_free_exception'
../libleanstatic.a(file_lock.cpp.o): In function `lean::file_lock::~file_lock()':
file_lock.cpp:(.text+0x325): undefined reference to `operator delete(void*)'
collect2: error: ld returned 1 exit status
make[2]: *** [shell/CMakeFiles/lean.dir/build.make:116: shell/lean] Error 1
make[1]: *** [CMakeFiles/Makefile2:2384: shell/CMakeFiles/lean.dir/all] Error 2
make: *** [Makefile:163: all] Error 2

[EdAyers]

Fixed with cmake -D CMAKE_CXX_COMPILER=g++-7 ../../src rookie error, I assumed gcc and g++ were the same. It builds now.

[kbuzzard]

just noting here that in the dupe thread https://github.com/leanprover/lean/issues/1966 someone has suggested a patch.