Jump to definition from a widget

Stream: metaprogramming / tactics

[Adam Topaz]

Do we have any examples of widgets that implement a jump-to-definition functionality?

[Anand Rao Tadipatri]

This code mimics the #check command and allows hovering over and clicking on the argument:

import Lean

open Lean Elab

elab "#" ι:ident : command =>
  for c in (← resolveGlobalConstWithInfos ι) do
    addCompletionInfo <| .id ι c (danglingDot := false) {} none

# Syntax

[Adam Topaz]

Thanks for this! But to clarify, I was referring to widgets in the sense of ProofWidgets. Namely, I want to figure out how to jump to definition from the infoview, from within a widget written in javascript.

[Utensil Song]

IIUC the code is in interactiveCode.

[Utensil Song]

It makes use of SelectableLocation etc. and is called from InteractiveCode in ProofWidgets.Component.Basic.

[Adam Topaz]

Thanks!

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Yep, the InteractiveCode and InteractiveExpr components are displayed in exactly the same way that expressions in the tactic state are, so go-to-definition should work there.

[Eric Wieser]

Is there an example of InteractiveCode anywhere?

[Adam Topaz]

There are some in the proofwidgets repo

[Adam Topaz]

https://github.com/leanprover-community/ProofWidgets4/blob/main/ProofWidgets/Demos/ExprPresentation.lean

[Utensil Song]

Some are as tsx, and some are as Lean DSL that mimics tsx, so they are easy to follow either in js or lean.

[Eric Wieser]

Maybe I should be clearer; if I just elaborated some Syntax (say, a tactic), how can I display that same syntax (with infotrees) in the widget view? The examples only show how to display an Expr.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

@Eric Wieser using docs4#Lean.MessageData.ofPPFormat (and, if lean4#3929 is merged, MessageData.ofFormatWithInfos), any Format object annotated with bits of Elab.Info can be displayed interactively (e.g. using ProofWidgets.InteractiveMessage). However, note that:

• only TermInfo and FieldInfo nodes are supported by the infoview; anything else might produce some unexpected behaviour
• there doesn't seem to be a function to pretty-print a tactic with info nodes: there is docs4#Lean.PrettyPrinter.ppTactic which produces a Format; you can still display that, but it wouldn't be interactive

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

The interactive display in the infoview uses different data structures than hovers/go-to-definitions/etc in the editor, so the sets of functionality are not equivalent.