search

leanprover / lean3

Lean Theorem Prover
http://leanprover.github.io/
Apache License 2.0
2.15k stars 217 forks source link

Are there linux install instructions? #2003

Closed enricozb closed 5 years ago

enricozb commented 5 years ago

I'd like to start to learn about theorem provers with lean. I downloaded the linux tarball, and found the executables lean, leanchecker and leanpkg inside lean-3.4.2/bin. I of course need to have my $PATH pointed to these executables, but I'm not sure what other environment variables to set up, especially since when running the lean executable, I am greeted with

test.lean:1:0: error: file 'init' not found in the LEAN_PATH
test.lean:1:0: error: invalid import: init
could not resolve import: init

What are the proper manual install instructions for linux?

enricozb commented 5 years ago

There are install instructions here.