Lean 4 outside of VS Code

Stream: general

[Dean Young]

Are there alternatives to VS Code in terms of running Lean 4?

For one thing, there is the online browser.

Is there an editor which can run Lean 4 interactively and natively besides VS Code?

[Henrik Böving]

"running Lean 4" is something that even your CLI can do without any editor. You can also use any editor which has LSP support and get somewhat of an experience. If you want the infoview as well then you are going to be limited to VScode, Neovim or Emacs

[Patrick Massot]

Sure, emacs and neovim can do that. There are a couple of things that currently work only in VSCode, but nothing mission critical unless you have very specific widget needs.

[Sebastian Ullrich]

Emacs does not have any infoview interactivity at all, that is a rather sizable limitation

[Patrick Massot]

Oh, I didn’t realize that. Neovim definitely has infoview interactivity.

[Simon Beaumont]

Sebastian Ullrich said:

Emacs does not have any infoview interactivity at all, that is a rather sizable limitation

Depends what you mean by interactivity, there is a PR from Richard Copley which adds the ability (via. magit-sections) to expand and collapse headings and jump to source lines. Not exactly infoview and javascript widgets but better than stock.

[Matthew Ballard]

Code actions?

[Matthew Ballard]

Though I went a year or so copying and pasting in neovim so I guess it is not necessary

[Sebastian Ullrich]

"Interactive diagnostics" are what we call the messages with embedded rich content such as expressions that you can interact with via hover etc.

[Richard Copley]

Simon Beaumont said:

Sebastian Ullrich said:

Emacs does not have any infoview interactivity at all, that is a rather sizable limitation

Depends what you mean by interactivity, there is a PR from Richard Copley which adds the ability (via. magit-sections) to expand and collapse headings and jump to source lines. Not exactly infoview and javascript widgets but better than stock.

@Paul Nelson's commits on his fork (and also on my fork) are more the thing that is being talked about here. Move point to an expression in the infoview, and its bounds will be highlighted and its type information displayed in the echo area (or *eldoc* buffer).

[Julian Berman]

(Emacs surely has code actions.)

[Paul Nelson]

I’ll add that by combining what @Richard Copley mentions with the embellishments at https://github.com/ultronozm/czm-lean4.el, you can effectively hover over anything in the info view with a documentation preview, “click on it” to jump to a dedicated window showing its documentation, hover over anything there in that window, and repeat the process indefinitely. For me, this is as useful as the VS code solution. Happy to help anyone interested get set up with this

[Shanghe Chen]

Hi with many helps from the community, I am currently working on a lean4 plugin for the intellij platform which is targeting to use lean4 interactively in IDE as Intellij Idea, PyCharm or Clion etc. It’s still on a very early stage and I am currently still trying to publish to the Jetbrains Marketplace, and still trying to fix bug, optimize performance etc. But currently interactive infoview/syntax highlight and unicode snippets do work! If anyone interested in this could download the latest release for a very early try

[dev luhar]

Shanghe Chen said:

Hi with many helps from the community, I am currently working on a lean4 plugin for the intellij platform which is targeting to use lean4 interactively in IDE as Intellij Idea, PyCharm or Clion etc. It’s still on a very early stage and I am currently still trying to publish to the Jetbrains Marketplace, and still trying to fix bug, optimize performance etc. But currently interactive infoview/syntax highlight and unicode snippets do work! If anyone interested in this could download the latest release for a very early try

how do i use mathlib with this plugin

[Shanghe Chen]

dev luhar said:

Shanghe Chen said:

Hi with many helps from the community, I am currently working on a lean4 plugin for the intellij platform which is targeting to use lean4 interactively in IDE as Intellij Idea, PyCharm or Clion etc. It’s still on a very early stage and I am currently still trying to publish to the Jetbrains Marketplace, and still trying to fix bug, optimize performance etc. But currently interactive infoview/syntax highlight and unicode snippets do work! If anyone interested in this could download the latest release for a very early try

how do i use mathlib with this plugin

Hi currently there’s still no libraries management or project management from the plugin inside IDE. For using mathlib you can add

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

to lakefile.lean under the root directory of your project and then run lake exe cache get in some terminal under the root directory of the project. After the cache downloaded successfully you should able to import files from mathlib expected. Thanks!