Using Lean from command line

Stream: general

[Arjun Viswanathan]

I have read this link about using Lean: https://leanprover.github.io/reference/using_lean.html
and am able to use Lean with VSCode, but I still have questions about using Lean from the command line.

1. When I download the lean binaries, there is a lean and leanchecker binary. What does each one do, and is there any documentation on using them?
2. What is LEAN_PATH? I wrote a Lean file that uses the Lean library list type. I want this to to be checked from the command-line, that is when I write a #check command in the file, on VSCode the #check is underlined in blue letting me know that it checks; I want to do the equivalent from the command-line. But when I run the Lean binary on my file, it says 'error: file 'data/list' not found in the LEAN_PATH'. Now, I have the entire Lean repository (https://github.com/leanprover/lean) in my system and it also contains the built binaries - this is what it took to get Lean to work on VSCode (that and telling VSCode where the head of the repository is). Also, the head of this repository is in my PATH but what does it mean for data/list to be in my LEAN_PATH?

I'm not able to find documentation for these specifics, most of them talk about using Lean from VSCode or Emacs. If I missed it, please point me to the right resource. Thanks!

[Patrick Massot]

If you create a Lean project the way described in https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md then there is no need to fiddle with LEAN_PATH. You can simply run lean from the root of your project.

[Arjun Viswanathan]

Thanks, useful as that is, I still want to understand how this works before having the package manager take care of the details for me. So I would still appreciate responses to my questions, if anybody is able to help.

[Reid Barton]

lean is Lean. You don't need leanchecker. You should also have leanpkg of course.

[Reid Barton]

There is no data.list in the Lean standard library. Are you trying to use mathlib?

[Patrick Massot]

leanpkg will create a leanpkg.path file in your project root folder. lean reads it, and you can read it as well, it's not hard to guess what it says.

[Kevin Buzzard]

You will have trouble with imports if you are running Lean on the command line and haven't set up a new project in the recommended way. However if you are only interested in lists and are happy with the list functionality of core Lean, you won't need to import anything.

The Lean binary runs Lean on a file and reports any errors, or, if there are none, compiles the file into bytecode (an .olean file). You can read Theorem Proving In Lean if you want to learn more about Lean.

[Arjun Viswanathan]

There is no data.list in the Lean standard library. Are you trying to use mathlib?

You're right, I was unintentionally using mathlib.

[Arjun Viswanathan]

Thanks for the responses. I'll just use lean in a project, as recommended. Is anybody able to tell me what the leanchecker binary is for?

[Reid Barton]

It's the Lean kernel in a standalone executable. It can read the files produced by lean --export. I doubt you'll find a use for it.

[Reid Barton]

We do use it in the mathlib automated test infrastructure as an extra sanity check. As far as I know it only ever catches when two definitions (in unrelated files) have the same name.

[Floris van Doorn]

And nowadays we even have a back-up test for that, since the sanity check creates a file that imports all other files, and therefore will also raise an error if two definitions have the same name.