Lean4 installation problems

Stream: new members

[Leandro Caniglia]

Even though I carefully installed VS Code (Windows) and followed the instructions for installing Lean4, I'm still unable to use it. Can someone figure out what I've done wrong? Thanks!

Some of the error messages I get:

1. Lean 4 server operating in restricted single file mode. Please open a valid Lean 4 project containing a 'lean-toolchain' file for full functionality.
2. 'Sandbox.lean' was closed in the meantime. Imports will not be rebuilt.
3. When trying #eval String.append("Hello, ", "Lean!") I get

Basic.lean:7:0
expression
  String.append
has type
  String → String → String
but instance
  Lean.Eval (String → String → String)
failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `Lean.Eval` class
Basic.lean:7:19
unexpected token '('; expected command

Clarification. I wrote the code in Basic.lean

[Mario Carneiro]

can you show a screenshot of the "explorer" view in vscode? What files exist and did you use "open folder" on the correct folder?

[Mario Carneiro]

the syntax #eval String.append("Hello, ", "Lean!") is incorrect, lean uses adjacency for function application so it should look like #eval String.append "Hello, " "Lean!" (or more conventionally #eval "Hello, " ++ "Lean!")

[Mario Carneiro]

Which instructions did you follow for installing lean4? (Could you link to it?)

[Leandro Caniglia]

image.png

I'm following Evaluating Expressions - Functional Programming in Lean (lean-lang.org)

[Leandro Caniglia]

The String.append issue is now clear. Thanks! Any idea of messages 1. and 2. above?

[Kevin Buzzard]

Have you created a valid Lean 4 project and tried using Lean on files within that project?

[Leandro Caniglia]

Yes. I clicked on the option to create a new Lean 4 project and that's why I now have the bunch of files shown in the screenshot.

[Kevin Buzzard]

The screenshot looks to me like things are working fine

[Tomas Uribe]

It appears you misread the manual : try #eval String.append "Hello, " "Lean!" instead. (The error message you posted is expected.)

[Leandro Caniglia]

Tomas Uribe said:

It appears you misread the manual : try #eval String.append "Hello, " "Lean!" instead.

Yes, you are right. Mario Carneiro already clarified it. Thanks!