Web Browsing from the Infoview

Stream: lean4

[Anand Rao Tadipatri]

I have written a small snippet of code to render the Mathlib4 docs in the Lean Infoview using the ProofWidgets4 framework. The intended use case is for looking up definitions and theorems in Mathlib4 without having to leave the Lean editor. Here is how it looks in VS Code (triggered by typing #docs):

docs_infoview.png

The code (available here) essentially creates an embedded HTML iframe with the Mathlib4 docs page as its source. The recommended way to try this code is by cloning and building the original ProofWidgets4 repository according to the instructions in the README and then pasting the following code in a file in ProofWidgets/Demos.

import ProofWidgets.Component.HtmlDisplay

open scoped ProofWidgets.Jsx

syntax (name := docsCmd) "#docs" : command

#html <iframe src="https://leanprover-community.github.io/mathlib4_docs/" width="100%" height="500px" frameborder="0"></iframe>

open Lean ProofWidgets Elab Command Server Json in
@[command_elab docsCmd]
def elabDocsCmd : CommandElab
  | stx@`(command| #docs) => do
    runTermElabM fun _ => do
      let docs := ProofWidgets.Html.ofTHtml <|
        <iframe src="https://leanprover-community.github.io/mathlib4_docs/"
            width="100%" height="600px" frameborder="0">
        </iframe>
      savePanelWidgetInfo stx ``HtmlDisplayPanel do
        return json% { html: $(← rpcEncode docs) }
  | _ => throwError "Unexpected syntax for rendering docs."

#docs

I find that some of the links - especially the ink and source buttons as well as the ones on the left sidebar - don't usually work when I click on them. This is probably a HTML iframe issue and not one specific to Lean or VS Code.

[Anand Rao Tadipatri]

I have now generalised the code to permit arbitrary browsing in the infoview. The new code contains two new commands - #browse and #web. The first takes in a URL as a string and renders the webpage in the infoview. The second takes in a name and a URL (for example, #web docs "https://leanprover-community.github.io/mathlib4_docs/") and creates a new command (#docs, in this example) for opening the chosen webpage.

Here are a few screenshots of the commands in VS Code:
browse_lean_blog_infoview.png
desmos_web_infoview.png

To try out the code, run the following sequence of commands in the terminal:

git clone https://github.com/0art0/ProofWidgets4 --branch browsing
cd ProofWidgets4
lake build :release

The above examples are contained in the file ProofWidgets/Demos/Docs.lean.

[Scott Morrison]

Does zulip work well in the infoview? I'd never leave VSCode again. :-)

[Anand Rao Tadipatri]

I tried, but unfortunately it doesn't load. It turns out that GitHub and Zulip (among other websites like Google) have taken measures to prevent their pages from being embedded as HTML iframes. Zulip may work if the HTML page is generated in a different way without iframes.

A bit of work will also be required to stay logged in to the same Zulip session across all files (I'm actually not sure if this is possible through Lean).