(The screenshot is taken from mathematics_in_lean)
and some video:
lean4ij-demo.mp4
A Lean4 plugin for the Intellij Platform.
This plugin uses LSP4IJ for connecting to the Lean4 lsp server. Please install that first.
-
Using the IDE built-in plugin system:
Settings/Preferences>Plugins>Marketplace>Search for "lean4ij">Install -
Manually: Download the latest release and install it manually using
Settings/Preferences>Plugins>⚙️>Install plugin from disk...
The plugin should be compatible from version 2024.1 and can not support the earlier versions for depending on textmate plugin's extension api.
For currently there is no functionality of creating a project or setting up a project. Before open any lean project with it please first testing if the project has set up the toolchain correctly. Run any command like elan which lake or lake exe cache get, etc.
The LSP server is start as any lean file is open in the Editor. If it not behaves correctly, try firing a restart action.
Unicode is supported via live templates, for example typing \b1<SPACE> would result in 𝟙. For the limitation of live templates, the <SPACE> keypress is always required.
Infoview is supported using lean4-infoview, and currently it can be started from a browser or the internal [JCEF] infoview toolwindow. If it not behaves correctly, try firing a restart action too.
Messages and logs about the lean lsp server can be found in the language server tool window after setting the level to message or trace, check more information about this in redhat-developer/lsp4ij.
| action id | action text | meaning |
|---|---|---|
| OpenLeanInfoView | Lean4 : Lean open info view | open the infoview(swing) |
| RestartLeanLsp | Lean4 : Restart Lean Lsp Server | restart the lsp server |
| RestartCurrentLeanFile | Lean4 : Restart Current Lean File | restart current file |
| RestartJcefInfoview | Lean4 : Restart Jcef Infoview | restart the jcef infoview |
Please check DEVELOP.md.
The plugin is still on an early stage, check ISSUES.md for known and logged issues.
and todos
- file progressing seems block UI thread in some cases
- solved by highlight on ranges rather than lines
- skip index
.lake/build - infoview toolwindow in swing
- show goals
- show term goal
- show message
- interactive message
- show all messages (all messages currently is skipped for not sure when it's trigger)
- interactive all messages
- popup
- pop up style, fonts, clickable links, etc
- color
- make the editor singleton
- mathlib4 seems always failed starting the language server this is because elan download lake while starting lsp, not fixed yet
- infoview toolwindow in jcef
- project create/setup or configuration
- distinguish source in .lake as library rather than source
- avoid file progressing in search window (it should be caused by didOpen, etc.) solved by only enable lsp at focusing editor
- setting dialog
- theme and color
- find in files will send a didOpen request and make fileProgress, it may hurt the performance. currently a fix for this is disabling lsp while lost focus for the editor
- elan/lake, project create, setup etc
- run and build (debug cannot be supported, although arend has this)
- some more logs with different levels
- refactor the frontend impl (currently it's written as for feasibility test)
- all messages in the external infoview failed (via caching server notification now)
- check why sometimes lsp requires multiple start
- all message should be interactive (check lean-infoview/src/infoview/info.tsx)
fixed via passing
hasWidgetswhen start lsp - jcef infoview style adjust
The following projects give great help for developing the plugin:
- leanprover/vscode-lean4
- leanprover-community/lean4web
- Julian/lean.nvim
- leanprover-community/lean4-mode
- redhat-developer/lsp4ij
Plugin based on the IntelliJ Platform Plugin Template.