List.range' not recognized

Stream: lean4

[Rudolf Meijer]

I get an error from the compiler " unknown constant List.range' ". According to the documentation this is a function with two arguments, which I have supplied. What is happening?

[James Gallicchio]

Could you put together a #mwe ? Makes it much easier for us to help :)

[James Gallicchio]

(But if I'm guessing randomly -- it's defined in Std, do you have import Std at the top of your file?)

[Rudolf Meijer]

I have Std imported. This is the MWE

import Std

def main : IO Unit := do
let stdout <- IO.getStdout
let range := (List.range' 1 5)
stdout.putStrLn (List.toString range)

[James Gallicchio]

Hum, that compiles fine for me

• are you working in a Lake project?
• are you using vscode?
• do you get output in the infoview if you write #eval Lean.versionString?

[Rudolf Meijer]

I am working in a Lake project. I am not using vscode. I don't know what is infoview, nor #eval. But the version is 4.0.0 alright (downloaded today)..

[Henrik Böving]

Just as a general remark without emacs, vim or vscode you're going to have a rather unhappy time with Lean really.

[Rudolf Meijer]

Actually, I use the Crimson editor, which at the touch of a button invokes Lake for me and shows me the output of the compilation and build process. What does vscode add?

[James Gallicchio]

Mainly you'll need something to show the InfoView-- which is the interactive display that a lot of Lean development is centered around. Emacs, VSCode and Vim have plugins that interact with the Lean language server to get the infoview information and display it.

[Rudolf Meijer]

Fine, I will see if I get vscode installed. But that does not explain the refusal of List.range' by the compiler. Am I missing some imports?

[James Gallicchio]

I'm still unsure about that. The file compiles fine for me in a default Lake project. Were you following setup instructions somewhere for the Lake project?

[Rudolf Meijer]

My lakefile.lean is

import Lake
open Lake DSL
package test {
  -- add package configuration options here
}
lean_lib Main {
  -- add library configuration options here
}
@[defaultTarget]
lean_exe test {
  root := `Main
}

and this file and Main.lean are in a folder test

I execute lake build test in the right folder.

[Kyle Miller]

Here's a quick start: https://github.com/leanprover/lean4/blob/master/doc/quickstart.md

[Kyle Miller]

But it's probably that you don't have Std as a dependency. You can add this to the end of your lakefile:

require std from git "https://github.com/leanprover/std4" @ "main"

[James Gallicchio]

I also suspect your Lean version is a bit out of date, since the Lakefile attribute is now called default_target. at the moment if you're working in Lean 4 you'll probably need to always make sure you're on the latest nightly.

The std4 @ main dependency will not compile on current nightly (there were a few breaking changes over the last couple months), & updating your Lean version to latest nightly is easier than finding what std commit compiles on your version.

[James Gallicchio]

sorry it's so fragile right now... the devs are trying to get everything ready for a stable release at breakneck speed :big_smile:

[Rudolf Meijer]

I have now followed the instructions and installed Lean via vscode. This is output in the Infoview for #eval Lean.versionString

"4.0.0-nightly-2023-01-13"

but for #eval List.range' 1 5 I get

unknown constant 'List.range''

Curious, isn't it. Should I import something?

[Arthur Paulino]

@Rudolf Meijer where's the definition of List.range' that you want to use? I mean, where have you seen it?

[Kyle Miller]

@Arthur Paulino It's List.range' in Std.Data.List.Basic

[Arthur Paulino]

Kyle Miller said:

But it's probably that you don't have Std as a dependency. You can add this to the end of your lakefile:

require std from git "https://github.com/leanprover/std4" @ "main"

That's needed in the lakefile.lean :point_up:

And then, on the file you want to call List.range', you need to import Std.Data.List.Basic at the top

[Rudolf Meijer]

I am not yet in a project, just typing in an untitled document. Is that the problem, that there is no lakefile.lean? In other words, does one always have to have a project?

[Rudolf Meijer]

Why is std not automatically required?

[Arthur Paulino]

If you want to use Lake to import dependencies, then yes, you need to be in a Lake project

[Mario Carneiro]

at least for now, std is just another package which has to be depended on and imported like everything else

[Rudolf Meijer]

But frankly, std is needed by everyone, I suppose.

[Mario Carneiro]

it does not have any special status of being bundled with lean

[Mario Carneiro]

this is primarily for developmental reasons

[Mario Carneiro]

it may change in the future but not any time soon

[Rudolf Meijer]

I see. I am learning... Sorry for assuming too much.

[Mario Carneiro]

std is also quite young compared to the core library (which is mainly focused on the tools required for the compiler itself)

[Mario Carneiro]

well, everything is young, it's a new language under active development

[Rudolf Meijer]

Also, do I need git ? lake protests when I type lake init ...

error: failed to execute `git`: no such file or directory (error code: 2)
warning: failed to initialize git repository

[Arthur Paulino]

A bit more on the topic: you may notice that some data structures have their Lean version as well as their Std version. Examples: HashMap and RBMap. Those have their Lean counterparts because, as Mario said they're needed for the compiler. So, if you need those structures but you really don't want to depend on Std, you can just import Lean.Data.RBMap or import Lean.Data.HashMap

[Arthur Paulino]

Rudolf Meijer said:

Also, do I need git ? lake protests when I type lake init ...

error: failed to execute `git`: no such file or directory (error code: 2)
warning: failed to initialize git repository

Yeah... lake init ... eventually calls git init -q here. But but it's not an obvious decision to me :thinking:

[Arthur Paulino]

Maybe the .gitignore addition as well as the call to git init -q should be optional as in lake init Foo --git?

[James Gallicchio]

I guess you could even get Lake to fetch dependencies without git, but that seems like a pain…

[Arthur Paulino]

However, since Lean 4 is pretty new, we still rely on other tools/languages to do things for us. For example, we need elan, which is implemented in Rust, to download toolchains. Lean 4 does not have its own host for packages yet so we (ab)use GitHub and rely on git to download packages for us. So yes, we pretty much assume you have git installed and set on your PATH otherwise you wouldn't even be able to ergonomically add Std as a dependency to your project.

[Arthur Paulino]

Hopefully, someday Lean 4 will have a bundled reliable implementation for performing HTTP requests

[Rudolf Meijer]

Meanwhile, I have found my way around all of this, and obtained my first result. This thread can be considered finshed. But I may be back with other questions, of course. :wink: