gcc 8.1.1: trie.h:69:76: error: ‘this’ was not captured for this lambda function

[andres-erbsen]

Prerequisites

• 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

On gcc 8.1.1 build fails with src/util/trie.h:69:76: error: ‘this’ was not captured for this lambda function.

Steps to Reproduce

at https://github.com/leanprover/lean/blob/master/doc/make/index.md#generic-build-instructions

Expected behavior: build succeeds

Actual behavior: build fails

Reproduces how often: always

Versions

browse@ashryn ~ % uname -a
Linux ashryn 4.17.10-1-ARCH #1 SMP PREEMPT Wed Jul 25 11:23:00 UTC 2018 x86_64 GNU/Linux
browse@ashryn ~ % gcc --version
gcc (GCC) 8.1.1 20180531

Additional Information

When building with clang 6.0.1, the same .c file succeeds (but generates warnings).

[spl]

See #1965.

[andres-erbsen]

A duplicate indeed. I'll leave it to the developers which one to leave open.

[spl]

I wouldn't expect this issue to be fixed soon. You're better off working around it. This is the current plan as stated in the README:

Lean 3.4.1 is the latest release. It is also the last release for the Lean 3.x code base. Only major bugs (e.g., soundness) will be fixed for this code base from now on. We are currently developing Lean 4 in a new (private) repository. The Lean 4 source code will be released here when ready.

[drvink]

I encountered this in June but didn't bother to report it, assuming a patch wouldn't be taken due to the aforementioned note that work on Lean 3.x is done. Since others are having the issue, here's my patch (yes, this actually fixes it):

diff --git a/src/util/trie.h b/src/util/trie.h
index 54d0695cd..1ea8854b7 100644
--- a/src/util/trie.h
+++ b/src/util/trie.h
@@ -56,7 +56,7 @@ class trie : public KeyCMP {
         }
     }
 
-    static trie merge(trie && t1, trie const & t2) {
+    static trie merge_(trie && t1, trie const & t2) {
         trie new_t1     = ensure_unshared(t1.steal());
         new_t1->m_value = t2->m_value;
         t2->m_children.for_each([&](Key const & k, trie const & c2) {
@@ -66,20 +66,20 @@ class trie : public KeyCMP {
                 } else {
                     trie n1(*c1);
                     new_t1->m_children.erase(k);
-                    new_t1->m_children.insert(k, trie::merge(n1.steal(), c2));
+                    new_t1->m_children.insert(k, trie::merge_(n1.steal(), c2));
                 }
             });
         return new_t1;
     }
 
     template<typename F>
-    static void for_each(F && f, trie const & n, buffer<Key> & prefix) {
+    static void for_each_(F && f, trie const & n, buffer<Key> & prefix) {
         if (n->m_value) {
             f(prefix.size(), prefix.data(), *(n->m_value));
         }
         n->m_children.for_each([&](Key const & k, trie const & c) {
                 prefix.push_back(k);
-                trie::for_each(f, c, prefix);
+                trie::for_each_(f, c, prefix);
                 prefix.pop_back();
             });
     }
@@ -134,14 +134,14 @@ public:
     }
 
     void merge(trie const & t) {
-        *this = merge(steal(), t);
+        *this = merge_(steal(), t);
     }
 
     template<typename F>
     void for_each(F && f) const {
         if (m_ptr) {
             buffer<Key> prefix;
-            for_each(f, *this, prefix);
+            for_each_(f, *this, prefix);
         }
     }