error with leanpkg - Githubissues

leanprover / lean3

Lean Theorem Prover

http://leanprover.github.io/

Apache License 2.0

2.15k stars 217 forks source link

error with leanpkg #1962

Closed blairshi111 closed 5 years ago

blairshi111 commented 6 years ago

Prerequisites

[ ] Put an X between the brackets on this line if you have done all of the following:
- Checked that your issue isn't already filed.
  - Specifically, check out the wishlist, open RFCs, or feature requests.
- Reduced the issue to a self-contained, reproducible test case.

Description

[Description of the issue] When I did leanpkg in my terminal, it reported many error like:

/usr/local/leanpkg/leanpkg/main.lean:1:0: error: file 'init' not found in the LEAN_PATH
/usr/local/leanpkg/leanpkg/toml.lean:1:0: error: file 'data/buffer/parser' not found in the LEAN_PATH
/usr/local/leanpkg/leanpkg/lean_version.lean:6:0: error: invalid import: init
could not resolve import: init

in my leanpkg.toml, it writes:

[package]
name = "xena-UROP-2018"
version = "0.1"
lean_version = "3.4.1"
path = "src"

[dependencies]
mathlib = {git = "https://github.com/leanprover/mathlib", rev = "905345a2ceaa5d0c7bc2f6310026961416b2cae4"}

Steps to Reproduce

[First Step] I typed leanpkg upgrade leanpkg build same error

Expected behavior: [What you expect to happen] I want to import mathlib.

Actual behavior: [What actually happens] I cannot import the file I need in mathlib.

Reproduces how often: [What percentage of the time does it reproduce?]

Versions

Lean (version 3.4.1, commit 17fe3decaf8a, Release) OS version 10.13.2

Additional Information

forked-from-1kasper commented 6 years ago

Did you make changes to LEAN_PATH? Did you add “[/path/to/lean]/lib/lean/library” to LEAN_PATH?