leanprover / lean2 Goto Github PK

Currently, Lean 2 cannot be compiled under newer versions of GCC (like 6.3 or 7). With GCC 7.1.1, it fails with the following error message:

[ 59%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/token_table.cpp.o
In file included from /tmp/lean2/src/frontends/lean/token_table.h:10:0,
                 from /tmp/lean2/src/frontends/lean/token_table.cpp:11:
/tmp/lean2/src/util/trie.h: In lambda function:
/tmp/lean2/src/util/trie.h:69:70: error: ‘this’ was not captured for this lambda function
                     new_t1->m_children.insert(k, merge(n1.steal(), c2));
                                                                      ^
/tmp/lean2/src/util/trie.h: In lambda function:
/tmp/lean2/src/util/trie.h:82:38: error: ‘this’ was not captured for this lambda function
                 for_each(f, c, prefix);
                                      ^
make[2]: *** [frontends/lean/CMakeFiles/lean_frontend.dir/build.make:87: frontends/lean/CMakeFiles/lean_frontend.dir/token_table.cpp.o] Error 1
make[1]: *** [CMakeFiles/Makefile2:2516: frontends/lean/CMakeFiles/lean_frontend.dir/all] Error 2
make: *** [Makefile:163: all] Error 2

In the commit d38979f 'unreachable' code was reached when elaborating this theorem on some machines:

This error occurred on a machine with Ubuntu 17.04 with g++ 6.3.0 or with g++ 5.4.1 (I believe) and on a mac (with unknown version gcc/g++).

There were no errors on a machine with Ubuntu 16.04 with gcc 5.4.0/g++ 5.4.0

The C++ spec requires the result of operator new to be aligned to alignof(max_align_t), which is 16 on x86_64 Linux. However, lean's operator new returns 8 byte aligned memory under tcmalloc, where malloc_usable_size, malloc_size and _msize are unavailable.
As clang assumes 16-byte-aligned memory and uses movaps for zero-filling, 8-byte-aligned memory causes a segmentation fault.

The 8-byte alignment is from lean::save_alloc_size in src/util/memory.cpp, that stores the size of allocation into a 8 byte leading region of the allocated memory chunk. So, to fix the alignment issue, the leading region should be alignof(max_align_t) instead of a single size_t.

It is quite difficult to read imaginaroid.lean since * is used both for multiplication and conjugation. May I suggest using ^ instead? This will improve readability a lot.

In algebra.md

The following code gives an ill-typed goal. More specifically, there is a variable pt in the goal (not to be confused with foo.pt) which is not in the local context. The code is for HoTT Lean, but the same error occurs in standard Lean if Type₀ is replaced by Type₁

prelude
import init.tactic
open unit

structure foo.{} (B : Type₀) (A : Type₀) : Type₀ :=
  (pt : B)

definition bar :=
foo unit

definition bar.mk [constructor] : bar unit :=
!foo.mk star
definition bar.mk2 [constructor] : bar unit :=
bar.mk

set_option pp.all true
example : eq (foo.pt (bar.mk2)) star :=
begin esimp end

Given output in release mode:

1 unsolved subgoal
⊢ @eq.{0} unit pt unit.star