Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Cannot build lean 3.4.2 #80034

Closed
Ailrun opened this issue Feb 13, 2020 · 1 comment · Fixed by #80167
Closed

Cannot build lean 3.4.2 #80034

Ailrun opened this issue Feb 13, 2020 · 1 comment · Fixed by #80167
Labels
0.kind: bug Something is broken

Comments

@Ailrun
Copy link
Contributor

Ailrun commented Feb 13, 2020

Describe the bug
It is not able to build lean 3.4.2 with

/build/source/library/init/meta/tactic.lean: parsing at line 1263terminate called after throwing an instance of 'lean::exception'
  what():  vm check failed: is_composite(o) (possibly due to incorrect axioms, or sorry)

To Reproduce
Steps to reproduce the behavior:

  1. nix-env -iA nixpkgs.lean

Expected behavior
Successfully build lean

Additional context
It looks like there is a build issue with lean 3.4.2 (leanprover/lean3#2006, leanprover-community/lean#62, leanprover-community/lean#77). It would be better to update lean to version 3.5.1 from https://github.com/leanprover-community/lean.

Metadata
Please run nix-shell -p nix-info --run "nix-info -m" and paste the result.

  • system: "x86_64-linux"
  • host os: Linux 5.4.18-1-MANJARO, Manjaro Linux, noversion
  • multi-user?: no
  • sandbox: yes
  • version: nix-env (Nix) 2.3.2
  • channels(jjc93): "nixpkgs-20.03pre211462.0c960262d15"
  • nixpkgs: /home/jjc93/.nix-defexpr/channels/nixpkgs

Maintainer information:

# a list of nixpkgs attributes affected by the problem
attribute:
# a list of nixos modules affected by the problem
module:
@Ailrun Ailrun added the 0.kind: bug Something is broken label Feb 13, 2020
@Ailrun
Copy link
Contributor Author

Ailrun commented Feb 13, 2020

I tried to update it locally, and failed. It still gives me what(): vm check failed: is_composite(o) (possibly due to incorrect axioms, or sorry).

@Ailrun Ailrun mentioned this issue Feb 15, 2020
10 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
0.kind: bug Something is broken
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant