Quick development with GitHub actions

For small change and quick development without Intellij Idea, you can use the GitHub actions to build and test the project. The following steps are required:

Fork the project or connect @onriv/@enigmurl for the privileges for this repo.
make any change in the forked repo and make a Pull Request to this repo, or push directly to the main branch in this repo if privileges for this repo are gained.
In the actions page, download the zip artifact for the latest successful build, and install it with the Intellij Idea.

This way it requires no local develop environment and can be done on any machine with internet access. But it requires some more time for the build and test process and hence it's only recommend for small changes.

Project and package structure

A brief description of current project and package structure

browser-infoview        : the frontend of external infoview
gradle                  : gradle wrapper
script                  : script that converts unicode to live templates
src/main/kotlin/lean4ij : main source of current implementation
├───actions             : actions (see Actions section in README.md)
├───infoview            : infoview implementation
│   └───external        : external infoview implementation
├───language            : currently textmate highlight and unicode live template
├───listeners           : a listener generated by intellij-plugin-template, not used
├───lsp                 : lsp client implementation
├───project             : project biz implementation
├───services            : a service generated by intellij-plugin-template, not used
└───util                : some utils

LSP

currently the project is using Lsp4ij to connect lean4 lsp server.

For some document on lean4 lsp server, please check

src/Lean/Server

Showing log in vscode with lean.trace.server set to verbose.

Highlight

The basic syntax highlight adapts the textmate syntax files from vscode-lean4/syntaxes/, using intelij platform sdk's textmate extension api and the implementation is at the class Lean4TextMateBundleProvider.

The sematic syntax highlight is transparently handled by lsp4ij and the lsp server and hence there is no code for this. Nevertheless there is some discussion on zulip saying there is some hacky part here, check Full BNF syntax?

Unicode input

The unicode input is implemented via live template. The template source is from vscode-lean4/lean4-unicode-input/src/abbreviations.json and using a script converting to intellij platform's format, the implement currently is at Lean4Language.kt.

InfoView

There is two infoview implementations currently:

the external infoview
the swing infoview

The external infoview

the external infoview is adapting lean4-infoview. The frontend source code is in the folder browser-infoview. The api is bridged to editor via a websocket connection. Check Route.kt file for this. The external infoview can be opened in a web browser and using JCEF embedding into the editor. Currently, the code is still very badly organized for requiring further development.

Build/Run/Debug the external infoview

If the gradle plugin cannot download the Node.js toolchains, then try change the option

download = false

download = true

and try to run the command npm install manually in the directory browser-infoview. Currently the Node.js version in used is 19.9.0

The internal/internal infoview

The swing/internal infoview is a raw infoview implemented using intellij platform's swing component. Although it can be implemented with rich components to make the style more beautiful like different fonts or size for the header etc. Currently the

Currently, the code is still very badly organized for requiring further development. The entrance point for rendering is at LeanFile.updateCaret which call LeanInfoViewWindowFactory.updateGoal when all lsp call finish.

The design for `TaggedText` and `InfoViewContent`

The implementation for the internal infoview, especially the render part needs big refactor.

Currently, the design for TaggedText and InfoviewContent is extremely complicated for not sure what the contract is.

The generic class TaggedText is original designed for respecting the following structure in the lean source code src/Lean/Widget/TaggedText.lean.

inductive TaggedText (α : Type u) where
  | text   : String → TaggedText α
  /-- Invariants:
  - non-empty
  - no adjacent `text` elements (they should be collapsed)
  - no directly nested `append`s (but `append #[tag _ (append ..)]` is okay) -/
  | append : Array (TaggedText α) → TaggedText α
  | tag    : α → TaggedText α → TaggedText α

That has three constructors. Here they are represented in three subclass: TaggedTextText, TaggedTextAppend and TaggedTextTag. For the type α in the above lean source code, currently it's the interface InfoViewContent and the implementations are

SubexprInfo
MsgEmbed
- MsgEmbedExpr
- MsgEmbedGoal
- MsgEmbedTrace
- MsgUnsupported

The implementation SubexprInfo corresponds to the following source code in the lean4 codebase in Lean/Widget/InteractiveCode.lean and is used for displaying interactive goals/expecting types in the infoview:

structure SubexprInfo where
  /-- The `Elab.Info` node with the semantics of this part of the output. -/
  info : WithRpcRef Lean.Elab.InfoWithCtx
  /-- The position of this subexpression within the top-level expression. See `Lean.SubExpr`. -/
  subexprPos : Lean.SubExpr.Pos
  -- TODO(WN): add fields for semantic highlighting
  -- kind : Lsp.SymbolKind
  /-- In certain situations such as when goal states change between positions in a tactic-mode proof,
  we can show subexpression-level diffs between two expressions. This field asks the renderer to
  display the subexpression as in a diff view (e.g. red/green like `git diff`). -/
  diffStatus? : Option DiffTag := none
  deriving RpcEncodable

The MsgEmbed and its subclasses are used for displaying the messages. Almost all complexities came from this part.

Developing in Intellij Idea

If the sync button does not work inside Intellij Idea, run ./gradlew sync in terminal first.

Proxy issue (this should only happen in some specific region) If the runPlugin task requires some proxy, create a file named local.properties and add the following content to it.

https.proxyHost=...
https.proxyPort=...

if using socks5 proxy then try the following code. Note that there is

socksProxyHost=127.0.0.1
socksProxyPort=7890

For first (and while require updating the frontend, run a gradle buildBrowserInfoview before run runIde). If the above way does not fix error in building the frontend, try remove nodeProxySettings = ProxySettings.FORCED too in build.gradle.kts.

Project Creating

Currently implementing, check https://plugins.jetbrains.com/docs/intellij/project-wizard.html for the official document.

Debug and troubleshooting

TODO

Test

The unittests are essential for regression while refactoring the codebase and implementing new features. Although currently there is little tests wrote in the project. Running it from gradle seems working fine currently, but for running a selected test in Intellij, add the following vm options. Check some test configuration files in the .run directory for detail.

--add-exports=java.base/jdk.internal.vm=ALL-UNNAMED
--add-exports=java.base/sun.util.calendar=ALL-UNNAMED
--add-exports=java.desktop/sun.awt=ALL-UNNAMED
--add-exports=jdk.scripting.nashorn/jdk.nashorn.internal.ir=ALL-UNNAMED
--add-opens=java.base/java.lang=ALL-UNNAMED
--add-opens=java.base/java.lang.module=ALL-UNNAMED
--add-opens=java.base/java.lang.reflect=ALL-UNNAMED
--add-opens=java.base/java.math=ALL-UNNAMED
--add-opens=java.base/java.nio=ALL-UNNAMED
--add-opens=java.base/java.text=ALL-UNNAMED
--add-opens=java.base/java.time=ALL-UNNAMED
--add-opens=java.base/java.util=ALL-UNNAMED
--add-opens=java.base/jdk.internal.jimage=ALL-UNNAMED
--add-opens=java.base/jdk.internal.jimage.decompressor=ALL-UNNAMED
--add-opens=java.base/jdk.internal.jrtfs=ALL-UNNAMED
--add-opens=java.base/jdk.internal.loader=ALL-UNNAMED
--add-opens=java.base/jdk.internal.math=ALL-UNNAMED
--add-opens=java.base/jdk.internal.module=ALL-UNNAMED
--add-opens=java.base/jdk.internal.perf=ALL-UNNAMED
--add-opens=java.base/jdk.internal.platform.cgroupv1=ALL-UNNAMED
--add-opens=java.base/jdk.internal.ref=ALL-UNNAMED
--add-opens=java.base/jdk.internal.reflect=ALL-UNNAMED
--add-opens=java.base/jdk.internal.util.jar=ALL-UNNAMED
--add-opens=java.base/jdk.internal.vm=ALL-UNNAMED
--add-opens=java.base/sun.nio.ch=ALL-UNNAMED
--add-opens=java.desktop/com.apple.eawt=ALL-UNNAMED
--add-opens=java.desktop/com.apple.eawt.event=ALL-UNNAMED
--add-opens=java.desktop/com.apple.laf=ALL-UNNAMED
--add-opens=java.desktop/java.awt=ALL-UNNAMED
--add-opens=java.desktop/java.awt.dnd.peer=ALL-UNNAMED
--add-opens=java.desktop/java.awt.event=ALL-UNNAMED
--add-opens=java.desktop/java.awt.image=ALL-UNNAMED
--add-opens=java.desktop/java.awt.peer=ALL-UNNAMED
--add-opens=java.desktop/javax.swing=ALL-UNNAMED
--add-opens=java.desktop/javax.swing.plaf.basic=ALL-UNNAMED
--add-opens=java.desktop/javax.swing.text.html=ALL-UNNAMED
--add-opens=java.desktop/sun.awt=ALL-UNNAMED
--add-opens=java.desktop/sun.awt.image=ALL-UNNAMED
--add-opens=java.desktop/sun.awt.windows=ALL-UNNAMED
--add-opens=java.desktop/sun.font=ALL-UNNAMED
--add-opens=java.desktop/sun.java2d=ALL-UNNAMED
--add-opens=java.desktop/sun.lwawt=ALL-UNNAMED
--add-opens=java.desktop/sun.lwawt.macosx=ALL-UNNAMED
--add-opens=java.desktop/sun.swing=ALL-UNNAMED
--add-opens=java.logging/sun.util.logging.internal=ALL-UNNAMED
--add-opens=java.xml/javax.xml.catalog=ALL-UNNAMED
--add-opens=java.xml/jdk.xml.internal=ALL-UNNAMED
--add-opens=jdk.attach/sun.tools.attach=ALL-UNNAMED
--add-opens=jdk.internal.jvmstat/sun.jvmstat.monitor=ALL-UNNAMED
--add-opens=jdk.jdi/com.sun.tools.jdi=ALL-UNNAMED
--add-opens=jdk.management/com.sun.management.internal=ALL-UNNAMED
--add-opens=jdk.management.jfr/jdk.management.jfr=ALL-UNNAMED
--add-opens=jdk.zipfs/jdk.nio.zipfs=ALL-UNNAMED
-Didea.force.use.core.classloader=true
-Djava.system.class.loader=com.intellij.util.lang.PathClassLoader
-ea

If a test failed in the pipeline, an artifact named "tests-result" will be generated at the part of artifacts and there is the detail for the failure of tests in it. Download and unzip to see the concrete error if necessary.

RELEASE

After the github action run, in the releases page there will be a draft release with the specified version. Edit it an make it a release or prerelease

Ref

Some ref on intellij plugin development

The general docs is at Intellij Platform SDK

For docs about extension points, check Extension Points and IntelliJ Platform Extension Point and Listener List

Related thread in zulip

Some threads in zulip during the developments:
- Would lsp server quit anomaly?
- elan which lake downloads lean if it not exist This is why currently the way to find the toolchain is manually done
- integrating infoview app
- Lean 4 outside of VS Code
- lsp fileProgress and gerInteractiveGoals
- lsp getInteractiveGoals and subexprPos?
- Full BNF syntax?
- using lean4-infoview alone inside an external browser
- ✔ Lean LSP extensions

Navigation Menu

Repository navigation

DEVELOP.md

DEVELOP.md

Quick development with GitHub actions

Project and package structure

LSP

Highlight

Unicode input

InfoView

The external infoview

Build/Run/Debug the external infoview

The internal/internal infoview

The design for `TaggedText` and `InfoViewContent`

Developing in Intellij Idea

Project Creating

Debug and troubleshooting

Test

RELEASE

Ref

Some ref on intellij plugin development

Related thread in zulip

FilesExpand file tree

DEVELOP.md

Latest commit

History

DEVELOP.md

File metadata and controls

Quick development with GitHub actions

Project and package structure

LSP

Highlight

Unicode input

InfoView

The external infoview

Build/Run/Debug the external infoview

The internal/internal infoview

The design for TaggedText and InfoViewContent

Developing in Intellij Idea

Project Creating

Debug and troubleshooting

Test

RELEASE

Ref

Some ref on intellij plugin development

Related thread in zulip

The design for `TaggedText` and `InfoViewContent`