This repository has been archived by the owner on Oct 14, 2023. It is now read-only.

build error: vm check failed: is_composite(o) #2006

Open

jwaldmann opened this issue Oct 31, 2019 · 1 comment

jwaldmann commented Oct 31, 2019

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

The text was updated successfully, but these errors were encountered:

Contributor

cipher1024 commented Oct 31, 2019

Can you repost to https://github.com/leanprover-community/lean? This is where we handle bug fixes now.

Ailrun mentioned this issue

Cannot build lean 3.4.2 NixOS/nixpkgs#80034

Closed

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.