leanprover / lean3

Lean Theorem Prover
http://leanprover.github.io/
Apache License 2.0
2.15k stars 217 forks source link

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

Open andres-erbsen opened 6 years ago

andres-erbsen commented 6 years ago

Prerequisites

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 commented 6 years ago

See #1965.

andres-erbsen commented 6 years ago

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

spl commented 6 years ago

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 commented 6 years ago

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);
         }
     }