build error: vm check failed: is_composite(o)
Opened this issue · 1 comments
jwaldmann commented
Hi. Building from source (git tag v3.4.2) on fedora-linux x86_64 with gcc-9.2.1, following instructions (using cmake then make) fails with
lean/library/init/meta/relation_tactics.lean: parsing at line 12terminate called after throwing an instance of 'lean::exception'
what(): vm check failed: is_composite(o) (possibly due to incorrect axioms, or sorry)
make[2]: *** [CMakeFiles/standard_lib.dir/build.make:57: CMakeFiles/standard_lib] Aborted
make[1]: *** [CMakeFiles/Makefile2:954: CMakeFiles/standard_lib.dir/all] Error 2
cipher1024 commented
Can you repost to https://github.com/leanprover-community/lean? This is where we handle bug fixes now.