language server

Stream: lean4

[Anders Christiansen Sørby]

I usually develop with nix and use nix develop to set LEAN_PATH and LEAN_SRC_PATH with the respective dependencies. I also add local directories with to LEAN_PATH, but this isn't perfect. Because the language server lean --server complains that there is no .olean files in the local dir. Why can't it just compile them? I want to make several improvements to the Lsp so that it becomes more nix friendly.

On a different note: Would it be possible to integrate the lean parser with tree-sitter so that one doesn't have to reimplement the parser there?

[Sebastian Ullrich]

You should not have to do any of this. lean-dev/emacs-dev/vscode-dev take care of compiling everything on the fly.

[Sebastian Ullrich]

Anders Christiansen Sørby said:

On a different note: Would it be possible to integrate the lean parser with tree-sitter so that one doesn't have to reimplement the parser there?

A static grammar like Tree-sitter's will never fully understand Lean's dynamic syntax. But writing a tool that generates a Tree-sitter grammar from a given set of Lean modules might be possible.

[Anders Christiansen Sørby]

Sebastian Ullrich said:

You should not have to do any of this. lean-dev/emacs-dev/vscode-dev take care of compiling everything on the fly.

Yes, but I'm using helix editor and it would be nice if the language server itself took care of generating olean files IMO.

[Anders Christiansen Sørby]

Now I have to do it manually with lean

[Sebastian Ullrich]

Then use lean-dev from your editor, just like emacs-dev and vscode-dev do

[Alex J. Best]

@Julian Berman has been working on a tree sitter parser iiuc https://github.com/Julian/tree-sitter-lean

[Anders Christiansen Sørby]

Sebastian Ullrich said:

You should not have to do any of this. lean-dev/emacs-dev/vscode-dev take care of compiling everything on the fly.

I missed that part. Maybe move/copy it to an editor specific section?

[Colin Roberts]

I am new to Lean 4 and I'm having a considerable amount of grief trying to even be able to work with this language in VSCode.

For example, working off of the greeting example in the text, I now bring in the mathlib as a dependency in my lakefile.lean:

import Lake
open Lake DSL

package «greeting» where
  -- add package configuration options here

lean_lib «Greeting» where
  -- add library configuration options here

@[default_target]
lean_exe «greeting» where
  root := `Main
  -- Enables the use of the Lean interpreter by the executable (e.g.,
  -- `runFrontend`) at the expense of increased binary size on Linux.
  -- Remove this line if you do not need such functionality.
  supportInterpreter := true

require mathlib from git
  "https://github.com/leanprover-community/mathlib4"

However, when I go to now work with Greeting/Basic.lean and start typing

import

I immediately am hit with an error: import failed, trying to import module with anonymous name instead of a tooltip, or suggestion, or anything I can work with. I don't see any suggestions for packages I can import here, just an error.

I followed the set up instructions to work with Lean 4 in VSCode, running on macOS. Just for sake of posterity, here are my versions:

❯ lean --version
Lean (version 4.7.0, aarch64-apple-darwin, commit 6fce8f7d5cd1, Release)

❯ elan --version
elan 3.1.1 (71ddc6633 2024-02-22)

❯ lake --version
Lake version 5.0.0-6fce8f7 (Lean version 4.7.0)

Am I doing something wrong here? What are the ways I can improve my developer experience in writing functional programs with Lean so that I can get the most out of a modern IDE?

I also apologize if this is not in the correct post location. This is my first post on the Lean 4 Zulip so please help me in suggesting the right place this should have gone! :grinning:

I look forward to being able to work with this language both for FP and proof assistance. I just need to get over the hump of setting up a DE for this!

[Kevin Buzzard]

It wouldn't surprise me at all if everything were working fine here. import by itself attempts to import a file with no name, which corresponds to the error message. Try import Lean?

[Marc Huisinga]

Colin Roberts said:

I am new to Lean 4 and I'm having a considerable amount of grief trying to even be able to work with this language in VSCode.

For example, working off of the greeting example in the text, I now bring in the mathlib as a dependency in my lakefile.lean:

import Lake
open Lake DSL

package «greeting» where
  -- add package configuration options here

lean_lib «Greeting» where
  -- add library configuration options here

@[default_target]
lean_exe «greeting» where
  root := `Main
  -- Enables the use of the Lean interpreter by the executable (e.g.,
  -- `runFrontend`) at the expense of increased binary size on Linux.
  -- Remove this line if you do not need such functionality.
  supportInterpreter := true

require mathlib from git
  "https://github.com/leanprover-community/mathlib4"

However, when I go to now work with Greeting/Basic.lean and start typing

import

I immediately am hit with an error: import failed, trying to import module with anonymous name instead of a tooltip, or suggestion, or anything I can work with. I don't see any suggestions for packages I can import here, just an error.

I followed the set up instructions to work with Lean 4 in VSCode, running on macOS. Just for sake of posterity, here are my versions:

❯ lean --version
Lean (version 4.7.0, aarch64-apple-darwin, commit 6fce8f7d5cd1, Release)

❯ elan --version
elan 3.1.1 (71ddc6633 2024-02-22)

❯ lake --version
Lake version 5.0.0-6fce8f7 (Lean version 4.7.0)

Am I doing something wrong here? What are the ways I can improve my developer experience in writing functional programs with Lean so that I can get the most out of a modern IDE?

I also apologize if this is not in the correct post location. This is my first post on the Lean 4 Zulip so please help me in suggesting the right place this should have gone! :grinning:

I look forward to being able to work with this language both for FP and proof assistance. I just need to get over the hump of setting up a DE for this!

What happens if you trigger the auto-completion after import using Ctrl+Space? (Option+Esc on MacOS, I believe)

[Kevin Buzzard]

PS this question is not quite in the right place -- you should start a new thread rather than just continuing someone else's on another question.