Lean 4 error: unknown package 'Leanpkg'

Stream: lean4

[Florin Dinu]

Hi! I'm new to Lean, I've installed it and can't run a simple script (both with nightly and stable toolchains). I've made a file called test.lean in which I wrote 2 lines

import Leanpkg
#eval Leanpkg.leanVersionString

When I run lean test.lean I get

test.lean:1:0: error: unknown package 'Leanpkg'
test.lean:2:6: error: unknown identifier 'Leanpkg.leanVersionString'
test.lean:2:0: error: unknown constant 'sorryAx'

On a side note, I'm using Ubuntu 22.04

[Kevin Buzzard]

Is your file part of a Lean project or did you just create a one-off file for testing?

[Florin Dinu]

I've just created it for testing

[Kevin Buzzard]

Then that's your problem. One-off files don't have a clue which version of Lean they're supposed to be using, or which packages they're supposed to be able to see.

[Kevin Buzzard]

One easy solution to this is to clone a project which is already set up correctly, for example Mathlib4 (my favourite lean 4 project, although I'm biased, I'm a mathematician).

[Kevin Buzzard]

If you clone this repo https://github.com/leanprover-community/mathlib4 with git clone git@github.com:leanprover-community/mathlib4.git and then make your test files in the resulting directory, things should work fine.

[Kevin Buzzard]

The idea is that this repository has a configuration file telling Lean which version of Lean to use and where to look for imports.

[Kevin Buzzard]

If you don't want to start downloading random repositories off the internet then you can make your own by going into a new directory and then typing lake init my_test_project to make all the configuration files. Then your imports should work

[Kevin Buzzard]

Actually I just tested both these methods and import Leanpkg doesn't work for either of them. Where are you seeing instructions to import this?

[Florin Dinu]

Thanks, it worked, I could run a file I got from a colleague. I was under the impression that I don't need to make a project, I can just use a file for testing.

As for the import Leanpkg, I've found it yesterday on a github issue and thought it might be the standard way to test a lean installation.

Anyway, it's time to do the tutorials so I won't ask any more questions like this. Thanks again.

[Kevin Buzzard]

Please feel free to ask many questions here; this is a very active Zulip and we're keen to onboard beginners.

[Kevin Buzzard]

You can ask them either here or in #new members

[Mario Carneiro]

leanpkg is a tool for managing lean 3 projects, which does not exist for lean 4. The analogous lean 4 project is lake and you don't need to import Lake in the main part of the project at all

[Arien Malec]

Have a look at the FPIL documentation and the Lake docu

[Arien Malec]

One thing that doesn't seem to be documented either place is that the root Lean directory needs to contain a single .lean file whose name is the same as your library, and any submodules are going to be placed in a directory named the same thing. So lean_lib Foo is going to have, in the same directory as the Lakefile, a single file Foo.lean, if submodules are required, a directory Foo, so that module Foo.Basic is going to be found in ./Foo/Basic.lean