An interactive display for the Lean 4 theorem prover.
The Lean 4 infoview is a React app providing an interactive display of messages, errors, proof states, and other outputs of Lean elaboration. Its capabilities can be extended using user widgets which may import @leanprover/infoview to access builtin functionality. This page contains technical information about how to embed the infoview in an editor plugin. For a friendly guide to user widgets, go here instead.
The infoview can be hosted within any LSP-compatible editor capable of displaying a webpage (e.g. a web-based editor, or via a WebKit panel, or in an external browser) and communicating with said webpage (e.g. via Window.postMessage). The hosting editor must also be capable of sending duplicates of received and emitted LSP notifications to the infoview, as well as of relaying LSP requests between the infoview and the LSP server. There are specific requirements on how the infoview code is loaded — see below.
⚠️ WARNING: Note that we have not tested the infoview outside of VSCode, so it is likely that a port to any other environment will need to generalize VSCode-specific parts.
Making user widgets dynamically loadable requires going through some contortions. The package exposes two entrypoints — @leanprover/infoview itself and @leanprover/infoview/loader. The former contains the React app. It is an ECMAScript module which must be loaded as a module into a runtime environment with:
- support for dynamic import; and
- a properly set up importmap.
In particular, @leanprover/infoview should not be transpiled into something like UMD by a bundler. To make this a bit easier, we provide the @leanprover/infoview/loader entrypoint which creates such an environment and loads the infoview into it. To use it, import it as usual (the loader can be bundled) and see documentation on the code.
(The alternative to using /loader is to embed the infoview in a webpage using